Interior and boundary of a manifold

Define the interior and boundary of a manifold.

Main definitions

• IsInteriorPoint x: x ∈ M is an interior point if, with φ being the preferred chart at x, φ x is an interior point of φ.target.
• IsBoundaryPoint x: x ∈ M is a boundary point if (extChartAt I x) x ∈ frontier (range I).
• interior I M is the interior of M, the set of its interior points.
• boundary I M is the boundary of M, the set of its boundary points.

Main results

• ModelWithCorners.univ_eq_interior_union_boundary: M is the union of its interior and boundary

• ModelWithCorners.interior_boundary_disjoint: interior and boundary of M are disjoint

• BoundarylessManifold.isInteriorPoint: if M is boundaryless, every point is an interior point

• ModelWithCorners.Boundaryless.boundary_eq_empty and of_boundary_eq_empty: M is boundaryless if and only if its boundary is empty

• isInteriorPoint_iff_of_mem_atlas: a point is an interior point iff any given chart around it sends it to the interior of the model; that is, the notion of interior is independent of choices of charts

• ModelWithCorners.isOpen_interior, ModelWithCorners.isClosed_boundary: the interior is open and and the boundary is closed. This is currently only proven for C¹ manifolds.

• ModelWithCorners.interior_open: the interior of u : Opens M is the preimage of the interior of M under the inclusion

• ModelWithCorners.boundary_open: the boundary of u : Opens M is the preimage of the boundary of M under the inclusion

• ModelWithCorners.BoundarylessManifold.open: if M is boundaryless, so is u : Opens M

• ModelWithCorners.interior_prod: the interior of M × N is the product of the interiors of M and N.

• ModelWithCorners.boundary_prod: the boundary of M × N is ∂M × N ∪ (M × ∂N).

• ModelWithCorners.BoundarylessManifold.prod: if M and N are boundaryless, so is M × N

• ModelWithCorners.interior_disjointUnion: the interior of a disjoint union M ⊔ M' is the union of the interior of M and M'

• ModelWithCorners.boundary_disjointUnion: the boundary of a disjoint union M ⊔ M' is the union of the boundaries of M and M'

• ModelWithCorners.boundaryless_disjointUnion: if M and M' are boundaryless, so is their disjoint union M ⊔ M'

Tags

manifold, interior, boundary

TODO

• the interior of M is dense, the boundary nowhere dense
• the interior of M is a boundaryless manifold
• boundary M is a submanifold (possibly with boundary and corners): follows from the corresponding statement for the model with corners I; this requires a definition of submanifolds
• if M is finite-dimensional, its boundary has measure zero
• generalise lemmas about C¹ manifolds with boundary to also hold for finite-dimensional topological manifolds; this will require e.g. the homology of spheres.

def ModelWithCorners.IsInteriorPoint {𝕜 : 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] (x : M) : Prop

p ∈ M is an interior point of a manifold M if and only if its image in the extended chart lies in the interior of the model space.

Equations

• I.IsInteriorPoint x = (↑(extChartAt I x) x ∈ interior (Set.range ↑I))

def ModelWithCorners.IsBoundaryPoint {𝕜 : 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] (x : M) : Prop

p ∈ M is a boundary point of a manifold M if and only if its image in the extended chart lies on the boundary of the model space.

Equations

• I.IsBoundaryPoint x = (↑(extChartAt I x) x ∈ frontier (Set.range ↑I))

def ModelWithCorners.interior {𝕜 : 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] : Set M

The interior of a manifold M is the set of its interior points.

Equations

• ModelWithCorners.interior M = {x : M | I.IsInteriorPoint x}

theorem ModelWithCorners.isInteriorPoint_iff {𝕜 : 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] {x : M} : I.IsInteriorPoint x ↔ ↑(extChartAt I x) x ∈ interior (extChartAt I x).target

def ModelWithCorners.boundary {𝕜 : 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] : Set M

The boundary of a manifold M is the set of its boundary points.

Equations

• ModelWithCorners.boundary M = {x : M | I.IsBoundaryPoint x}

theorem ModelWithCorners.isBoundaryPoint_iff {𝕜 : 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] {x : M} : I.IsBoundaryPoint x ↔ ↑(extChartAt I x) x ∈ frontier (Set.range ↑I)

theorem ModelWithCorners.isInteriorPoint_or_isBoundaryPoint {𝕜 : 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] (x : M) : I.IsInteriorPoint x ∨ I.IsBoundaryPoint x

Every point is either an interior or a boundary point.

theorem ModelWithCorners.interior_union_boundary_eq_univ {𝕜 : 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] : ModelWithCorners.interior M ∪ ModelWithCorners.boundary M = Set.univ

A manifold decomposes into interior and boundary.

theorem ModelWithCorners.disjoint_interior_boundary {𝕜 : 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] : Disjoint (ModelWithCorners.interior M) (ModelWithCorners.boundary M)

The interior and boundary of a manifold M are disjoint.

theorem ModelWithCorners.isInteriorPoint_iff_not_isBoundaryPoint {𝕜 : 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] (x : M) : I.IsInteriorPoint x ↔ ¬I.IsBoundaryPoint x

theorem ModelWithCorners.compl_interior {𝕜 : 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] : (ModelWithCorners.interior M)ᶜ = ModelWithCorners.boundary M

The boundary is the complement of the interior.

theorem ModelWithCorners.compl_boundary {𝕜 : 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] : (ModelWithCorners.boundary M)ᶜ = ModelWithCorners.interior M

The interior is the complement of the boundary.

theorem range_mem_nhds_isInteriorPoint {𝕜 : 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] {x : M} (h : I.IsInteriorPoint x) : Set.range ↑I ∈ nhds (↑(extChartAt I x) x)

class BoundarylessManifold {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_7} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_8) [TopologicalSpace M] [ChartedSpace H M] : Prop

Type class for manifold without boundary. This differs from ModelWithCorners.Boundaryless, which states that the ModelWithCorners maps to the whole model vector space.

• isInteriorPoint' (x : M) : I.IsInteriorPoint x

instance ModelWithCorners.instBoundarylessManifold {𝕜 : 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] [I.Boundaryless] : BoundarylessManifold I M

Boundaryless ModelWithCorners implies boundaryless manifold.

instance ModelWithCorners.BoundarylessManifold.of_empty {𝕜 : 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] [IsEmpty M] : BoundarylessManifold I M

The empty manifold is boundaryless.

theorem BoundarylessManifold.isInteriorPoint {𝕜 : 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] {x : M} [BoundarylessManifold I M] : I.IsInteriorPoint x

theorem ModelWithCorners.interior_eq_univ {𝕜 : 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] [BoundarylessManifold I M] : ModelWithCorners.interior M = Set.univ

If I is boundaryless, M has full interior.

theorem ModelWithCorners.Boundaryless.boundary_eq_empty {𝕜 : 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] [BoundarylessManifold I M] : ModelWithCorners.boundary M = ∅

Boundaryless manifolds have empty boundary.

instance ModelWithCorners.instIsEmptyElemBoundaryOfBoundarylessManifold {𝕜 : 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] [BoundarylessManifold I M] : IsEmpty ↑(ModelWithCorners.boundary M)

theorem ModelWithCorners.Boundaryless.iff_boundary_eq_empty {𝕜 : 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] : ModelWithCorners.boundary M = ∅ ↔ BoundarylessManifold I M

M is boundaryless if and only if its boundary is empty.

theorem ModelWithCorners.Boundaryless.of_boundary_eq_empty {𝕜 : 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] (h : ModelWithCorners.boundary M = ∅) : BoundarylessManifold I M

Manifolds with empty boundary are boundaryless.

theorem DifferentiableAt.mem_interior_convex_of_surjective_fderiv {E : Type u_5} {H : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup H] [NormedSpace ℝ H] {f : E → H} {x : E} (hf : DifferentiableAt ℝ f x) {u : Set E} (hu : u ∈ nhds x) {s : Set H} (hs : Convex ℝ s) (hs' : IsClosed s) (hs'' : (interior s).Nonempty) (hfus : Set.MapsTo f u s) (hfx : Function.Surjective ⇑(fderiv ℝ f x)) : f x ∈ interior s

If a function f : E → H is differentiable at x, sends a neighbourhood u of x to a closed convex set s with nonempty interior and has surjective differential at x, it must send x to the interior of s.

theorem ModelWithCorners.mem_interior_range_of_mem_interior_range_of_mem_atlas {𝕜 : 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] {n : WithTop ℕ∞} [IsManifold I n M] {e e' : OpenPartialHomeomorph M H} {x : M} (hn : n ≠ 0) (he : e ∈ atlas H M) (he' : e' ∈ atlas H 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 any two charts e, e' around a point x in a C¹ manifold, if e maps x to the interior of the model space, e' does too - in other words, the notion of interior points does not depend on any choice of charts.

Note that in general, this is actually quite nontrivial; that is why are focusing only on C¹ manifolds here. For merely topological finite-dimensional manifolds the proof involves singular homology, and for infinite-dimensional topological manifolds I don't even know if this lemma holds.

theorem ModelWithCorners.mem_interior_range_iff_of_mem_atlas {𝕜 : 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] {n : WithTop ℕ∞} [IsManifold I n M] {e e' : OpenPartialHomeomorph M H} {x : M} (hn : n ≠ 0) (he : e ∈ atlas H M) (he' : e' ∈ atlas H M) (hex : x ∈ e.source) (hex' : x ∈ e'.source) : ↑(e.extend I) x ∈ interior (e.extend I).target ↔ ↑(e'.extend I) x ∈ interior (e'.extend I).target

For any two charts e, e' around a point x in a C¹ manifold, e maps x to the interior of the model space iff e' does. - in other words, the notion of interior points does not depend on any choice of charts.

theorem ModelWithCorners.isInteriorPoint_iff_of_mem_atlas {𝕜 : 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] {n : WithTop ℕ∞} [IsManifold I n M] {e : OpenPartialHomeomorph M H} {x : M} (hn : n ≠ 0) (he : e ∈ atlas H M) (hx : x ∈ e.source) : I.IsInteriorPoint x ↔ ↑(e.extend I) x ∈ interior (e.extend I).target

A point x in a C¹ manifold is an interior point if and only if it gets mapped to the interior of the model space by any given chart - in other words, the notion of interior points does not depend on any choice of charts.

theorem ModelWithCorners.isBoundaryPoint_iff_of_mem_atlas {𝕜 : 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] {n : WithTop ℕ∞} [IsManifold I n M] {e : OpenPartialHomeomorph M H} {x : M} (hn : n ≠ 0) (he : e ∈ atlas H M) (hx : x ∈ e.source) : I.IsBoundaryPoint x ↔ ↑(e.extend I) x ∈ frontier (e.extend I).target

A point x in a C¹ manifold is a boundary point if and only if it gets mapped to the boundary of the model space by any given chart - in other words, the notion of boundary points does not depend on any choice of charts.

Also see ModelWithCorners.isInteriorPoint_iff_of_mem_atlas.

theorem ModelWithCorners.isOpen_interior {𝕜 : 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] {n : WithTop ℕ∞} [IsManifold I n M] (hn : n ≠ 0) : IsOpen (ModelWithCorners.interior M)

The interior of any C¹ manifold is open.

This is currently only proven for C¹ manifolds, but holds at least for finite-dimensional topological manifolds too; see ModelWithCorners.isInteriorPoint_iff_of_mem_atlas.

theorem ModelWithCorners.isClosed_boundary {𝕜 : 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] {n : WithTop ℕ∞} [IsManifold I n M] (hn : n ≠ 0) : IsClosed (ModelWithCorners.boundary M)

The boundary of any C¹ manifold is closed.

This is currently only proven for C¹ manifolds, but holds at least for finite-dimensional topological manifolds too; see ModelWithCorners.isInteriorPoint_iff_of_mem_atlas.

Interior and boundary of open subsets of a manifold.

theorem ModelWithCorners.isInteriorPoint_iff_isInteriorPoint_val {𝕜 : 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] {u : TopologicalSpace.Opens M} {x : ↥u} : I.IsInteriorPoint x ↔ I.IsInteriorPoint ↑x

For u : Opens M, x : u is an interior point iff x.val : M is.

theorem ModelWithCorners.isBoundaryPoint_iff_isBoundaryPoint_val {𝕜 : 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] {u : TopologicalSpace.Opens M} {x : ↥u} : I.IsBoundaryPoint x ↔ I.IsBoundaryPoint ↑x

For u : Opens M, x : u is a boundary point iff x.val : M is.

theorem ModelWithCorners.interior_open {𝕜 : 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] {u : TopologicalSpace.Opens M} : ModelWithCorners.interior ↥u = Subtype.val ⁻¹' ModelWithCorners.interior M

The interior of u : Opens M is the preimage of the interior of M under the inclusion.

theorem ModelWithCorners.boundary_open {𝕜 : 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] {u : TopologicalSpace.Opens M} : ModelWithCorners.boundary ↥u = Subtype.val ⁻¹' ModelWithCorners.boundary M

The boundary of u : Opens M is the preimage of the boundary of M under the inclusion.

instance ModelWithCorners.BoundarylessManifold.open {𝕜 : 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] [BoundarylessManifold I M] (u : TopologicalSpace.Opens M) : BoundarylessManifold I ↥u

Open subsets of boundaryless manifolds are boundaryless.

Interior and boundary of the product of two manifolds.

theorem ModelWithCorners.interior_prod {𝕜 : 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] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {J : ModelWithCorners 𝕜 E' H'} : ModelWithCorners.interior (M × N) = ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N

The interior of M × N is the product of the interiors of M and N.

theorem ModelWithCorners.boundary_prod {𝕜 : 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] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {J : ModelWithCorners 𝕜 E' H'} : ModelWithCorners.boundary (M × N) = Set.univ.prod (ModelWithCorners.boundary N) ∪ (ModelWithCorners.boundary M).prod Set.univ

The boundary of M × N is ∂M × N ∪ (M × ∂N).

theorem ModelWithCorners.boundary_of_boundaryless_left {𝕜 : 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] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {J : ModelWithCorners 𝕜 E' H'} [BoundarylessManifold I M] : ModelWithCorners.boundary (M × N) = Set.univ.prod (ModelWithCorners.boundary N)

If M is boundaryless, ∂(M×N) = M × ∂N.

theorem ModelWithCorners.boundary_of_boundaryless_right {𝕜 : 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] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {J : ModelWithCorners 𝕜 E' H'} [BoundarylessManifold J N] : ModelWithCorners.boundary (M × N) = (ModelWithCorners.boundary M).prod Set.univ

If N is boundaryless, ∂(M×N) = ∂M × N.

instance ModelWithCorners.BoundarylessManifold.prod {𝕜 : 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] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {J : ModelWithCorners 𝕜 E' H'} [BoundarylessManifold I M] [BoundarylessManifold J N] : BoundarylessManifold (I.prod J) (M × N)

The product of two boundaryless manifolds is boundaryless.

Interior and boundary of the disjoint union of two manifolds.

theorem ModelWithCorners.interiorPoint_inl {𝕜 : 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] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M'] (x : M) (hx : I.IsInteriorPoint x) : I.IsInteriorPoint (Sum.inl x)

theorem ModelWithCorners.boundaryPoint_inl {𝕜 : 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] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M'] (x : M) (hx : I.IsBoundaryPoint x) : I.IsBoundaryPoint (Sum.inl x)

theorem ModelWithCorners.interiorPoint_inr {𝕜 : 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] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M'] (x : M') (hx : I.IsInteriorPoint x) : I.IsInteriorPoint (Sum.inr x)

theorem ModelWithCorners.boundaryPoint_inr {𝕜 : 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] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M'] (x : M') (hx : I.IsBoundaryPoint x) : I.IsBoundaryPoint (Sum.inr x)

theorem ModelWithCorners.isInteriorPoint_disjointUnion_left {𝕜 : 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] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M'] {p : M ⊕ M'} (hp : I.IsInteriorPoint p) (hleft : p.isLeft = true) : I.IsInteriorPoint (p.getLeft hleft)

theorem ModelWithCorners.isInteriorPoint_disjointUnion_right {𝕜 : 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] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M'] {p : M ⊕ M'} (hp : I.IsInteriorPoint p) (hright : p.isRight = true) : I.IsInteriorPoint (p.getRight hright)

theorem ModelWithCorners.interior_disjointUnion {𝕜 : 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] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M'] : ModelWithCorners.interior (M ⊕ M') = Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M'

theorem ModelWithCorners.boundary_disjointUnion {𝕜 : 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] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M'] : ModelWithCorners.boundary (M ⊕ M') = Sum.inl '' ModelWithCorners.boundary M ∪ Sum.inr '' ModelWithCorners.boundary M'

instance ModelWithCorners.boundaryless_disjointUnion {𝕜 : 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] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M'] [hM : BoundarylessManifold I M] [hM' : BoundarylessManifold I M'] : BoundarylessManifold I (M ⊕ M')

If M and M' are boundaryless, so is their disjoint union M ⊔ M'.