Chart-independent detection of manifold boundary points

This file restates Mathlib's chart-independence results for interior and boundary points against the range of a model with corners. This is the form used when computing the boundary of a concrete model.

Mathlib states chart independence for charts of the atlas. The charts produced by local normal forms, such as the charts of Manifold.IsImmersionAt, are only known to lie in the maximal atlas, so the statements here are proved for every chart of IsManifold.maximalAtlas. Membership in the maximal atlas makes a chart a local diffeomorphism, so Mathlib's IsLocalDiffeomorphAt.isInteriorPoint_iff gives chart independence without a global IsManifold assumption on the charted space.

theorem TauCeti.ModelWithCorners.isInteriorPoint_iff_mem_interior_range {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {k : WithTop ℕ∞} {e : OpenPartialHomeomorph M H} {x : M} (hk : k ≠ 0) (he : e ∈ IsManifold.maximalAtlas I k M) (hx : x ∈ e.source) : I.IsInteriorPoint x ↔ ↑I (↑e x) ∈ interior (Set.range ↑I)

An interior point of a charted space is detected by any maximal-atlas chart around it, provided its differentiability exponent is nonzero.

theorem TauCeti.ModelWithCorners.mem_interior_extend_target_of_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {k : WithTop ℕ∞} {e e' : OpenPartialHomeomorph M H} {x : M} (hk : k ≠ 0) (he : e ∈ IsManifold.maximalAtlas I k M) (he' : e' ∈ IsManifold.maximalAtlas I k M) (hex : x ∈ e.source) (hex' : x ∈ e'.source) (hx : ↑(e.extend I) x ∈ interior (e.extend I).target) : ↑(e'.extend I) x ∈ interior (e'.extend I).target

For two charts of the maximal atlas with nonzero differentiability exponent around a point x, if the first reads x in the interior of its extended target, so does the second.

theorem TauCeti.ModelWithCorners.isBoundaryPoint_iff_mem_frontier_range {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {k : WithTop ℕ∞} {e : OpenPartialHomeomorph M H} {x : M} (hk : k ≠ 0) (he : e ∈ IsManifold.maximalAtlas I k M) (hx : x ∈ e.source) : I.IsBoundaryPoint x ↔ ↑I (↑e x) ∈ frontier (Set.range ↑I)

A boundary point of a charted space is detected by any maximal-atlas chart around it, provided its differentiability exponent is nonzero.