InteriorBoundary

📁 Source: Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean

Statistics

Metric	Count
Definitions `BoundarylessManifold`, `IsBoundaryPoint`, `IsInteriorPoint`, `boundary`, `interior`	5
Theorems `isInteriorPoint`, `isInteriorPoint'`, `boundary_eq_empty`, `iff_boundary_eq_empty`, `of_boundary_eq_empty`, `of_empty`, `open`, `prod`, `boundaryPoint_inl`, `boundaryPoint_inr`, `boundary_disjointUnion`, `boundary_of_boundaryless_left`, `boundary_of_boundaryless_right`, `boundary_open`, `boundary_prod`, `boundaryless_disjointUnion`, `compl_boundary`, `compl_interior`, `disjoint_interior_boundary`, `instBoundarylessManifold`, `instIsEmptyElemBoundaryOfBoundarylessManifold`, `interiorPoint_inl`, `interiorPoint_inr`, `interior_disjointUnion`, `interior_eq_univ`, `interior_open`, `interior_prod`, `interior_union_boundary_eq_univ`, `isBoundaryPoint_iff`, `isBoundaryPoint_iff_isBoundaryPoint_val`, `isInteriorPoint_disjointUnion_left`, `isInteriorPoint_disjointUnion_right`, `isInteriorPoint_iff`, `isInteriorPoint_iff_isInteriorPoint_val`, `isInteriorPoint_iff_not_isBoundaryPoint`, `isInteriorPoint_or_isBoundaryPoint`, `range_mem_nhds_isInteriorPoint`	37
Total	42

BoundarylessManifold

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isInteriorPoint` 📖	mathematical	—	`ModelWithCorners.IsInteriorPoint`	—	`isInteriorPoint'`
`isInteriorPoint'` 📖	mathematical	—	`ModelWithCorners.IsInteriorPoint`	—	—

ModelWithCorners

Definitions

Name	Category	Theorems
`IsBoundaryPoint` 📖	MathDef	6 math math: `isInteriorPoint_or_isBoundaryPoint`, `Icc_isBoundaryPoint_bot`, `isInteriorPoint_iff_not_isBoundaryPoint`, `isBoundaryPoint_iff_isBoundaryPoint_val`, `isBoundaryPoint_iff`, `Icc_isBoundaryPoint_top`
`IsInteriorPoint` 📖	MathDef	7 math math: `isInteriorPoint_or_isBoundaryPoint`, `BoundarylessManifold.isInteriorPoint`, `Icc_isInteriorPoint_interior`, `isInteriorPoint_iff_isInteriorPoint_val`, `isInteriorPoint_iff_not_isBoundaryPoint`, `BoundarylessManifold.isInteriorPoint'`, `isInteriorPoint_iff`
`boundary` 📖	CompOp	14 math math: `compl_boundary`, `instIsEmptyElemBoundaryOfBoundarylessManifold`, `interior_union_boundary_eq_univ`, `boundary_open`, `Boundaryless.iff_boundary_eq_empty`, `boundary_disjointUnion`, `Boundaryless.boundary_eq_empty`, `compl_interior`, `boundary_of_boundaryless_left`, `boundary_of_boundaryless_right`, `boundary_prod`, `disjoint_interior_boundary`, `boundary_Icc`, `boundary_product`
`interior` 📖	CompOp	8 math math: `compl_boundary`, `interior_open`, `interior_eq_univ`, `interior_disjointUnion`, `interior_union_boundary_eq_univ`, `compl_interior`, `disjoint_interior_boundary`, `interior_prod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`boundaryPoint_inl` 📖	mathematical	`IsBoundaryPoint`	`instTopologicalSpaceSum` `ChartedSpace.sum`	—	`isBoundaryPoint_iff` `extChartAt.eq_1` `nonempty_of_chartedSpace` `Topology.IsOpenEmbedding.inl` `ChartedSpace.sum_chartAt_inl` `Function.Injective.extend_apply` `Sum.inl_injective`
`boundaryPoint_inr` 📖	mathematical	`IsBoundaryPoint`	`instTopologicalSpaceSum` `ChartedSpace.sum`	—	`isBoundaryPoint_iff` `extChartAt.eq_1` `nonempty_of_chartedSpace` `Topology.IsOpenEmbedding.inr` `ChartedSpace.sum_chartAt_inr` `Function.Injective.extend_apply` `Sum.inr_injective`
`boundary_disjointUnion` 📖	mathematical	—	`boundary` `instTopologicalSpaceSum` `ChartedSpace.sum` `Set` `Set.instUnion` `Set.image`	—	`interior_disjointUnion` `Set.inl_compl_union_inr_compl`
`boundary_of_boundaryless_left` 📖	mathematical	—	`boundary` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `prod` `instTopologicalSpaceProd` `prodChartedSpace` `Set.prod` `Set.univ`	—	`boundary_prod` `Boundaryless.boundary_eq_empty` `Set.empty_prod` `Set.union_empty`
`boundary_of_boundaryless_right` 📖	mathematical	—	`boundary` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `prod` `instTopologicalSpaceProd` `prodChartedSpace` `Set.prod` `Set.univ`	—	`boundary_prod` `Boundaryless.boundary_eq_empty` `Set.prod_empty` `Set.empty_union`
`boundary_open` 📖	mathematical	—	`boundary` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype` `TopologicalSpace.Opens.instChartedSpace` `Set.preimage`	—	`compl_interior` `interior_open`
`boundary_prod` 📖	mathematical	—	`boundary` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `prod` `instTopologicalSpaceProd` `prodChartedSpace` `Set` `Set.instUnion` `Set.prod` `Set.univ`	—	`compl_interior` `interior_prod` `Set.compl_prod_eq_union` `Set.union_comm`
`boundaryless_disjointUnion` 📖	mathematical	—	`BoundarylessManifold` `instTopologicalSpaceSum` `ChartedSpace.sum`	—	`Boundaryless.iff_boundary_eq_empty` `boundary_disjointUnion` `Set.image_empty` `Set.union_self`
`compl_boundary` 📖	mathematical	—	`Compl.compl` `Set` `Set.instCompl` `boundary` `interior`	—	`compl_interior` `compl_compl`
`compl_interior` 📖	mathematical	—	`Compl.compl` `Set` `Set.instCompl` `interior` `boundary`	—	`compl_unique` `Set.disjoint_iff_inter_eq_empty` `disjoint_interior_boundary` `interior_union_boundary_eq_univ`
`disjoint_interior_boundary` 📖	mathematical	—	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `interior` `boundary`	—	`Set.not_disjoint_iff` `Set.mem_empty_iff_false` `Set.disjoint_iff_inter_eq_empty` `disjoint_interior_frontier` `Set.mem_inter_iff`
`instBoundarylessManifold` 📖	mathematical	—	`BoundarylessManifold`	—	`IsOpen.interior_eq` `OpenPartialHomeomorph.isOpen_extend_target` `isInteriorPoint_iff` `PartialEquiv.map_source` `mem_extChartAt_source`
`instIsEmptyElemBoundaryOfBoundarylessManifold` 📖	mathematical	—	`IsEmpty` `Set.Elem` `boundary`	—	`Set.isEmpty_coe_sort` `Boundaryless.boundary_eq_empty`
`interiorPoint_inl` 📖	mathematical	`IsInteriorPoint`	`instTopologicalSpaceSum` `ChartedSpace.sum`	—	`isInteriorPoint_iff` `extChartAt.eq_1` `nonempty_of_chartedSpace` `Topology.IsOpenEmbedding.inl` `ChartedSpace.sum_chartAt_inl` `Function.Injective.extend_apply` `Sum.inl_injective` `target_eq` `interior_inter`
`interiorPoint_inr` 📖	mathematical	`IsInteriorPoint`	`instTopologicalSpaceSum` `ChartedSpace.sum`	—	`isInteriorPoint_iff` `extChartAt.eq_1` `nonempty_of_chartedSpace` `Topology.IsOpenEmbedding.inr` `ChartedSpace.sum_chartAt_inr` `Function.Injective.extend_apply` `Sum.inr_injective` `target_eq` `interior_inter`
`interior_disjointUnion` 📖	mathematical	—	`interior` `instTopologicalSpaceSum` `ChartedSpace.sum` `Set` `Set.instUnion` `Set.image`	—	—
`interior_eq_univ` 📖	mathematical	—	`interior` `Set.univ`	—	`Set.eq_univ_of_forall` `BoundarylessManifold.isInteriorPoint`
`interior_open` 📖	mathematical	—	`interior` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype` `TopologicalSpace.Opens.instChartedSpace` `Set.preimage`	—	`Set.ext` `isInteriorPoint_iff_isInteriorPoint_val`
`interior_prod` 📖	mathematical	—	`interior` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `prod` `instTopologicalSpaceProd` `prodChartedSpace` `SProd.sprod` `Set` `Set.instSProd`	—	`Set.ext` `interior_prod_eq` `Set.range_prodMap` `modelWithCorners_prod_coe` `IsInteriorPoint.eq_1` `Set.mem_prod` `interior.eq_1`
`interior_union_boundary_eq_univ` 📖	mathematical	—	`Set` `Set.instUnion` `interior` `boundary` `Set.univ`	—	`Set.eq_univ_of_forall` `Set.mem_union` `isInteriorPoint_or_isBoundaryPoint`
`isBoundaryPoint_iff` 📖	mathematical	—	`IsBoundaryPoint` `Set` `Set.instMembership` `frontier` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `toFun'` `PartialEquiv.toFun` `extChartAt`	—	—
`isBoundaryPoint_iff_isBoundaryPoint_val` 📖	mathematical	—	`IsBoundaryPoint` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype` `TopologicalSpace.Opens.instChartedSpace`	—	`isInteriorPoint_iff_not_isBoundaryPoint` `isInteriorPoint_iff_isInteriorPoint_val`
`isInteriorPoint_disjointUnion_left` 📖	—	`IsInteriorPoint` `instTopologicalSpaceSum` `ChartedSpace.sum`	—	—	`boundaryPoint_inl` `isInteriorPoint_iff_not_isBoundaryPoint`
`isInteriorPoint_disjointUnion_right` 📖	—	`IsInteriorPoint` `instTopologicalSpaceSum` `ChartedSpace.sum`	—	—	`Set.mem_empty_iff_false` `Disjoint.inter_eq` `disjoint_interior_boundary` `interior.eq_1` `Set.mem_setOf` `boundary.eq_1` `isInteriorPoint_or_isBoundaryPoint` `boundaryPoint_inr`
`isInteriorPoint_iff` 📖	mathematical	—	`IsInteriorPoint` `Set` `Set.instMembership` `interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.target` `extChartAt` `PartialEquiv.toFun`	—	`OpenPartialHomeomorph.mem_interior_extend_target` `mem_chart_target` `OpenPartialHomeomorph.interior_extend_target_subset_interior_range`
`isInteriorPoint_iff_isInteriorPoint_val` 📖	mathematical	—	`IsInteriorPoint` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype` `TopologicalSpace.Opens.instChartedSpace`	—	`isInteriorPoint_iff` `TopologicalSpace.Opens.chartAt_eq` `target_eq` `TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_target` `interior_inter` `OpenPartialHomeomorph.extend_preimage_mem_nhds` `mem_chart_source` `IsOpen.mem_nhds` `TopologicalSpace.Opens.is_open'`
`isInteriorPoint_iff_not_isBoundaryPoint` 📖	mathematical	—	`IsInteriorPoint` `IsBoundaryPoint`	—	`Set.mem_empty_iff_false` `Set.disjoint_iff_inter_eq_empty` `disjoint_interior_frontier` `Set.mem_inter_iff` `isInteriorPoint_or_isBoundaryPoint`
`isInteriorPoint_or_isBoundaryPoint` 📖	mathematical	—	`IsInteriorPoint` `IsBoundaryPoint`	—	`IsInteriorPoint.eq_1` `isBoundaryPoint_iff` `closure_diff_interior` `IsClosed.closure_eq` `isClosed_range` `Set.mem_diff` `Set.mem_range_self`

ModelWithCorners.Boundaryless

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`boundary_eq_empty` 📖	mathematical	—	`ModelWithCorners.boundary` `Set` `Set.instEmptyCollection`	—	`ModelWithCorners.compl_interior` `ModelWithCorners.interior_eq_univ` `Set.compl_empty_iff`
`iff_boundary_eq_empty` 📖	mathematical	—	`ModelWithCorners.boundary` `Set` `Set.instEmptyCollection` `BoundarylessManifold`	—	`Set.compl_empty_iff` `ModelWithCorners.compl_interior` `boundary_eq_empty`
`of_boundary_eq_empty` 📖	mathematical	`ModelWithCorners.boundary` `Set` `Set.instEmptyCollection`	`BoundarylessManifold`	—	`iff_boundary_eq_empty`

ModelWithCorners.BoundarylessManifold

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_empty` 📖	mathematical	—	`BoundarylessManifold`	—	`IsEmpty.false`
`open` 📖	mathematical	—	`BoundarylessManifold` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype` `TopologicalSpace.Opens.instChartedSpace`	—	`ModelWithCorners.isInteriorPoint_iff_isInteriorPoint_val` `BoundarylessManifold.isInteriorPoint`
`prod` 📖	mathematical	—	`BoundarylessManifold` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`ModelWithCorners.Boundaryless.of_boundary_eq_empty` `ModelWithCorners.boundary_prod` `ModelWithCorners.Boundaryless.boundary_eq_empty` `Set.prod_empty` `Set.empty_prod`

(root)

Definitions

Name	Category	Theorems
`BoundarylessManifold` 📖	CompData	9 math math: `ModelWithCorners.instBoundarylessManifold`, `ModelWithCorners.Boundaryless.of_boundary_eq_empty`, `ModelWithCorners.Boundaryless.iff_boundary_eq_empty`, `SingularManifold.boundaryless`, `SingularManifold.instBoundarylessManifoldRealM`, `ModelWithCorners.BoundarylessManifold.of_empty`, `ModelWithCorners.BoundarylessManifold.open`, `ModelWithCorners.boundaryless_disjointUnion`, `ModelWithCorners.BoundarylessManifold.prod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`range_mem_nhds_isInteriorPoint` 📖	mathematical	`ModelWithCorners.IsInteriorPoint`	`Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `Set.range` `ModelWithCorners.toFun'`	—	`mem_nhds_iff` `interior_subset` `isOpen_interior`

---

← Back to Index