Clopen parts of closed submanifolds #
A part of a closed submanifold Y that is open in Y and closed in the ambient manifold — a
clopen part of Y, written Y ∩ O with O open — is a closed submanifold of the same
codimension: its adapted charts are the adapted charts of Y restricted to O. Not in the
sources; used where a centre is a union of some of the components of an intersection of boundary
hypersurfaces (Hironaka/Resolution/Analytic/Principalization/SncClopen.lean).
theorem
Manifold.IsAdaptedChart.inter_restrOpen
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
[ChartedSpace E M]
{Y : Set M}
{φ : OpenPartialHomeomorph M E}
{c : ℕ}
{σ : Fin c ↪ Fin n}
(h : IsAdaptedChart ψ Y φ σ)
{O : Set M}
(hO : IsOpen O)
:
IsAdaptedChart ψ (Y ∩ O) (φ.restrOpen O hO) σ
The restriction of an adapted chart of Y to an open set O is an adapted chart of the
clopen part Y ∩ O.
theorem
Manifold.IsClosedSubmanifold.inter_of_isOpen
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
[ChartedSpace E M]
{Y : Set M}
{c : ℕ}
(hY : IsClosedSubmanifold ψ Y c)
{O : Set M}
(hO : IsOpen O)
(hZ : IsClosed (Y ∩ O))
:
IsClosedSubmanifold ψ (Y ∩ O) c
A closed part of a closed submanifold that is open in it is a closed submanifold of the same codimension.