A closed submanifold is a manifold

With the charts induced by the adapted charts — the complementary coordinates, IsAdaptedChart.chartOn — a closed submanifold Y of codimension c is an analytic manifold modelled on 𝕜^{n-c} (Bierstone–Milman: a smooth subspace of a manifold "is a manifold and is locally a coordinate subspace of a coordinate chart" [BM97, (3.8)(2)]). The chart change between two induced charts is the chart change φ₂ ∘ φ₁⁻¹ of M (analytic, both charts being in the maximal atlas) conjugated by the linear maps ψ⁻¹ ∘ embedCompl and projCompl ∘ ψ (chartChange_contDiffOn), so it lies in the analytic groupoid (chartChange_mem); hence the induced charted space is a manifold (isManifold') and every chart induced by an adapted chart is in its maximal atlas (chartOn_mem_maximalAtlas'). Also here: mem_contDiffGroupoid_self, the criterion for an open partial homeomorphism of a normed space to lie in the analytic groupoid. The manifold structure on Y is what makes a centre, a hypersurface of maximal contact or a stratum of the boundary an analytic manifold in its own right.

theorem Manifold.contDiff_embedCompl {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) : ContDiff 𝕜 ⊤ (embedCompl σ)

The inclusion 𝕜^{n-c} → 𝕜^n along the coordinates outside σ is analytic (it is linear).

theorem Manifold.contDiff_projCompl {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) : ContDiff 𝕜 ⊤ (projCompl σ)

The projection 𝕜^n → 𝕜^{n-c} onto the coordinates outside σ is analytic (it is linear).

theorem Manifold.mem_contDiffGroupoid_self {𝕜 : Type} [RCLike 𝕜] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : OpenPartialHomeomorph F F) (h : ContDiffOn 𝕜 ⊤ (↑e) e.source) (h' : ContDiffOn 𝕜 ⊤ (↑e.symm) e.target) : e ∈ contDiffGroupoid ⊤ (modelWithCornersSelf 𝕜 F)

An open partial homeomorphism of a normed space that is analytic with analytic inverse lies in the analytic groupoid of the model space.

theorem Manifold.contDiffOn_chartChange {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {φ₁ φ₂ : OpenPartialHomeomorph M E} (h₁ : φ₁ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (h₂ : φ₂ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : ContDiffOn 𝕜 ⊤ (↑φ₂ ∘ ↑φ₁.symm) (φ₁.target ∩ ↑φ₁.symm ⁻¹' φ₂.source)

The chart change of two charts of the maximal atlas is analytic.

theorem Manifold.IsAdaptedChart.chartChange_contDiffOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Y : Set M} {c : ℕ} {φ₁ φ₂ : OpenPartialHomeomorph M E} {σ₁ σ₂ : Fin c ↪ Fin n} (h₁ : IsAdaptedChart ψ Y φ₁ σ₁) {a₁ : M} (ha₁ : a₁ ∈ Y) (h₂ : IsAdaptedChart ψ Y φ₂ σ₂) {a₂ : M} (ha₂ : a₂ ∈ Y) : ContDiffOn 𝕜 ⊤ (↑((h₁.chartOn ha₁).symm.trans (h₂.chartOn ha₂))) ((h₁.chartOn ha₁).symm.trans (h₂.chartOn ha₂)).source

The chart change between two induced charts of Y is analytic on its domain.

theorem Manifold.IsAdaptedChart.chartChange_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Y : Set M} {c : ℕ} {φ₁ φ₂ : OpenPartialHomeomorph M E} {σ₁ σ₂ : Fin c ↪ Fin n} (h₁ : IsAdaptedChart ψ Y φ₁ σ₁) {a₁ : M} (ha₁ : a₁ ∈ Y) (h₂ : IsAdaptedChart ψ Y φ₂ σ₂) {a₂ : M} (ha₂ : a₂ ∈ Y) : (h₁.chartOn ha₁).symm.trans (h₂.chartOn ha₂) ∈ contDiffGroupoid ⊤ (modelWithCornersSelf 𝕜 (Fin (n - c) → 𝕜))

The chart change between two induced charts lies in the analytic groupoid.

theorem Manifold.IsClosedSubmanifold.isManifold' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : IsManifold (modelWithCornersSelf 𝕜 (Fin (n - c) → 𝕜)) ⊤ ↑Y

With the induced charts, a closed submanifold is an analytic manifold modelled on 𝕜^{n-c} [BM97, (3.8)(2)].

theorem Manifold.IsAdaptedChart.chartOn_mem_maximalAtlas' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (h : IsAdaptedChart ψ Y φ σ) {a : M} (ha : a ∈ Y) : h.chartOn ha ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 (Fin (n - c) → 𝕜)) ⊤ ↑Y

Every chart of Y induced by an adapted chart is a chart of the maximal atlas of Y.