Documentation

Mathlib.Geometry.Manifold.InteriorBoundary

Interior and boundary of a manifold #

Define the interior and boundary of a manifold.

Main definitions #

Main results #

Tags #

manifold, interior, boundary

TODO #

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) :

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
Instances For
    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) :

    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
    Instances For
      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
      • I.interior M = {x : M | I.IsInteriorPoint x}
      Instances For
        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
        • I.boundary M = {x : M | I.IsBoundaryPoint x}
        Instances For
          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] :
          I.interior M I.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 (I.interior M) (I.boundary M)

          The interior and boundary of a manifold M are disjoint.

          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] :
          (I.interior M) = I.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] :
          (I.boundary M) = I.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] :

          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
            theorem BoundarylessManifold.isInteriorPoint' {𝕜 : Type u_5} :
            ∀ {inst : NontriviallyNormedField 𝕜} {E : Type u_6} {inst_1 : NormedAddCommGroup E} {inst_2 : NormedSpace 𝕜 E} {H : Type u_7} {inst_3 : TopologicalSpace H} {I : ModelWithCorners 𝕜 E H} {M : Type u_8} {inst_4 : TopologicalSpace M} {inst_5 : ChartedSpace H M} [self : BoundarylessManifold I M] (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] :

            Boundaryless ModelWithCorners implies boundaryless manifold.

            Equations
            • =

            The empty manifold is boundaryless.

            Equations
            • =
            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] :
            I.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] :
            I.boundary M =

            Boundaryless manifolds have empty boundary.

            Equations
            • =

            M is boundaryless iff 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 : I.boundary M = ) :

            Manifolds with empty boundary 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') :
            (I.prod J).interior (M × N) = I.interior M ×ˢ J.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') :
            (I.prod J).boundary (M × N) = Set.univ.prod (J.boundary N) (I.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] :
            (I.prod J).boundary (M × N) = Set.univ.prod (J.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] :
            (I.prod J).boundary (M × N) = (I.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.

            Equations
            • =