The strict transform of a clopen part #
The strict transform closure (π⁻¹(H ∖ Z)) of a clopen part H ∩ O of a closed set H under a
continuous map π is the corresponding clopen part π⁻¹(O) of the strict transform of H
(strictTransformSet_inter_of_isOpen). This is used for the pieces of the boundary divisor in the
order-reduction algorithm (clopen parts of the members of the boundary): the strict transform of a
piece is a clopen part of the strict transform of its member, hence a closed hypersurface when the
member's strict transform is one. A point-set lemma, not in the sources.
theorem
Manifold.strictTransformSet_inter_of_isOpen
{M : Type u}
[TopologicalSpace M]
{M' : Type u}
[TopologicalSpace M']
{π : M' → M}
(hπ : Continuous π)
(Z : Set M)
{H O : Set M}
(hO : IsOpen O)
(hHO : IsClosed (H ∩ O))
:
The strict transform of a clopen part H ∩ O of a closed set H is the part π⁻¹(O) of the
strict transform of H.