ModelWithCorners.disjoint_interior_boundary
theorem ModelWithCorners.disjoint_interior_boundary :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M],
Disjoint (I.interior M) (I.boundary M)
This theorem states that the interior and the boundary of a manifold `M` are disjoint, given a model with corners `I`. In other words, there is no element that belongs to both the interior and the boundary of the manifold `M` in the given model. This theorem is valid in the context of a `NontriviallyNormedField 𝕜`, a `NormedAddCommGroup E`, a `NormedSpace 𝕜 E`, a `TopologicalSpace H`, a `TopologicalSpace M`, and a `ChartedSpace H M`. Disjointness in this context is defined as the property that for all elements `x` in our set, if `x` is less than or equal to `a` and `x` is less than or equal to `b`, then `x` must be less than or equal to the bottom element.
More concisely: The interior and boundary of a manifold M in a given model with no elements in common.
|
ModelWithCorners.boundary_eq_complement_interior
theorem ModelWithCorners.boundary_eq_complement_interior :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M], I.boundary M = (I.interior M)ᶜ
This theorem states that the boundary of a given model with corners is equal to the complement of the interior of that same model. Here, a model with corners over a field `𝕜` is a topological space that is equipped with a smooth structure that makes it behave like the Euclidean space near each point. The boundary and the interior of the model are defined in the context of this smooth structure. The theorem holds for any model with corners `I` over a nontrivially normed field `𝕜`, with the model mapping to a normed additive commutative group `E` under a normed space structure, and for any topological space `M` that is charted over topological space `H` with the help of `I`.
More concisely: The boundary of a model with corners over a nontrivially normed field equals the complement of its interior in the ambient topological space, under the given smooth structure and charting over a Hausdorff space.
|
ModelWithCorners.isInteriorPoint_or_isBoundaryPoint
theorem ModelWithCorners.isInteriorPoint_or_isBoundaryPoint :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (x : M),
I.IsInteriorPoint x ∨ I.IsBoundaryPoint x
This theorem states that for any given point in a topological space, under a model with corners (a mathematical framework used in differential geometry), that point is either an interior point or a boundary point. This applies to any point `x` in a topological space `M`, which is modeled with corners `I` over a field `𝕜` with a norm, a normed additive commutative group `E`, and another topological space `H`. This theorem asserts a fundamental property of topological spaces, dividing all points into interior points, which are completely inside a set, and boundary points, which lie on the edge of a set.
More concisely: In a topological space modeled with corners over a normed field, every point is either an interior point or a boundary point.
|
ModelWithCorners.Boundaryless.boundary_eq_empty
theorem ModelWithCorners.Boundaryless.boundary_eq_empty :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : BoundarylessManifold I M],
I.boundary M = ∅
This theorem states that for any boundaryless manifold M, under a given ModelWithCorners I, the boundary of M is empty. This is true for all normed fields 𝕜, normed additive commutative group E, and topological space H. The manifold M is assumed to be a topological space that is charted on H, and the ModelWithCorners I is between 𝕜, E, and H.
More concisely: For any boundaryless manifold M modeled between a normed field 𝕜, a normed additive commutative group E, and a topological space H with charting topological space H, the boundary of M is empty.
|
BoundarylessManifold.isInteriorPoint
theorem BoundarylessManifold.isInteriorPoint :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : BoundarylessManifold I M]
{x : M}, I.IsInteriorPoint x
This theorem states that for any point `x` in a boundaryless manifold `M` (equipped with a topological structure), the point is an interior point according to the model with corners `I`. More formally, given a nontrivial normed field `𝕜`, a normed additive commutative group `E`, a topological space `H`, and a model with corners `I` that associates these structures, any point `x` in a boundaryless manifold `M` (that is modeled on the space `H` with the model `I`) is an interior point as per the definition given by the model with corners `I`.
More concisely: Any point in a boundaryless manifold modeled on a normed additive commutative group with a topology using a model with corners is an interior point according to the model.
|
ModelWithCorners.interior_eq_univ
theorem ModelWithCorners.interior_eq_univ :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : BoundarylessManifold I M],
I.interior M = Set.univ
This theorem states that for any nontrivially normed field 𝕜, any normed addition-commutative group E, any normed space of 𝕜 and E, and any topological space H, if a model with corners I is defined on 𝕜, E, and H, and for any type M which is a topological space and a charted space on H, if the manifold defined by I and M has no boundary (is boundaryless), then the interior of M with respect to the model with corners I is equal to the universal set. This means that the set M fully occupies the interior of the space defined by the model with corners I.
More concisely: For any nontrivially normed field 𝕜, normed addition-commutative group E, normed space F over 𝕜 and E, and topological space H with a model with corners I, if M is a boundaryless charted topological space on H, then the interior of M with respect to I is equal to the universal set H.
|
ModelWithCorners.interior_union_boundary_eq_univ
theorem ModelWithCorners.interior_union_boundary_eq_univ :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M],
I.interior M ∪ I.boundary M = Set.univ
This theorem states that for any non-trivially normed field `𝕜`, any normed additively commutative group `E` that is a normed space over `𝕜`, any topological space `H`, any model with corners `I` of type `ModelWithCorners 𝕜 E H`, any topological space `M` and any charted space `M` with model `H`, the union of the interior and the boundary of `M` with respect to `I` forms the universal set. In other words, a manifold decomposes into its interior and its boundary, covering all points in the space.
More concisely: For any non-trivially normed field `𝕜`, any normed additively commutative group `E` over `𝕜`, any topological space `H`, any model with corners `I` of type `ModelWithCorners 𝕜 E H`, and any charted space `M` with model `H`, the interior and boundary of `M` with respect to `I` form the universal set. (I.e., every point in the space is in the interior or the boundary of some chart in `M`.)
|