Interior and boundary of a manifold #
Define the interior and boundary of a manifold.
Main definitions #
- IsInteriorPoint x:
p ∈ M
is an interior point if, forφ
being the preferred chart atx
,φ x
is an interior point ofφ.target
. - IsBoundaryPoint x:
p ∈ 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 boundaryModelWithCorners.interior_boundary_disjoint
: interior and boundary ofM
are disjointBoundarylessManifold.isInteriorPoint
: ifM
is boundaryless, every point is an interior pointModelWithCorners.Boundaryless.boundary_eq_empty
andof_boundary_eq_empty
:M
is boundaryless if and only if its boundary is emptyModelWithCorners.interior_prod
: the interior ofM × N
is the product of the interiors ofM
andN
.ModelWithCorners.boundary_prod
: the boundary ofM × N
is∂M × N ∪ (M × ∂N)
.ModelWithCorners.BoundarylessManifold.prod
: ifM
andN
are boundaryless, so isM × N
Tags #
manifold, interior, boundary
TODO #
x
is an interior point iff any chart aroundx
maps it tointerior (range I)
; similarly for the boundary.- the interior of
M
is open, hence the boundary is closed (and nowhere dense) In finite dimensions, this requires e.g. the homology of spheres. - the interior of
M
is a smooth manifold without boundary boundary M
is a smooth submanifold (possibly with boundary and corners): follows from the corresponding statement for the model with cornersI
; this requires a definition of submanifolds- if
M
is finite-dimensional, its boundary has measure zero
p ∈ M
is an interior point of a manifold M
iff 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))
Instances For
p ∈ M
is a boundary point of a manifold M
iff 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))
Instances For
The interior of a manifold M
is the set of its interior points.
Equations
- I.interior M = {x : M | I.IsInteriorPoint x}
Instances For
The boundary of a manifold M
is the set of its boundary points.
Equations
- I.boundary M = {x : M | I.IsBoundaryPoint x}
Instances For
Every point is either an interior or a boundary point.
A manifold decomposes into interior and boundary.
The interior and boundary of a manifold M
are disjoint.
The boundary is the complement of the interior.
The interior is the complement of the boundary.
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
Instances
Boundaryless ModelWithCorners
implies boundaryless manifold.
Equations
- ⋯ = ⋯
The empty manifold is boundaryless.
Equations
- ⋯ = ⋯
If I
is boundaryless, M
has full interior.
Boundaryless manifolds have empty boundary.
Equations
- ⋯ = ⋯
M
is boundaryless iff its boundary is empty.
Manifolds with empty boundary are boundaryless.
Interior and boundary of the product of two manifolds.
The interior of M × N
is the product of the interiors of M
and N
.
The boundary of M × N
is ∂M × N ∪ (M × ∂N)
.
If M
is boundaryless, ∂(M×N) = M × ∂N
.
If N
is boundaryless, ∂(M×N) = ∂M × N
.
The product of two boundaryless manifolds is boundaryless.
Equations
- ⋯ = ⋯