InteriorBoundary

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

Statistics

Metric	Count
Definitions `BoundarylessManifold`, `IsBoundaryPoint`, `IsInteriorPoint`, `boundary`, `interior`	5
Theorems `isInteriorPoint`, `isInteriorPoint'`, `boundarylessManifold`, `boundarylessManifold_iff`, `image_boundary`, `image_interior`, `preimage_boundary`, `preimage_interior`, `mem_interior_convex_of_surjective_fderiv`, `boundarylessManifold`, `preimage_boundary`, `preimage_interior`, `isBoundaryPoint_iff`, `isInteriorPoint_iff`, `preimage_boundary_inter`, `preimage_interior_inter`, `isInteriorPoint_of_surjective_mfderiv`, `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`, `isBoundaryPoint_iff_not_isInteriorPoint`, `isBoundaryPoint_iff_of_mem_atlas`, `isClosed_boundary`, `isInteriorPoint_disjointUnion_left`, `isInteriorPoint_disjointUnion_right`, `isInteriorPoint_iff`, `isInteriorPoint_iff_isInteriorPoint_val`, `isInteriorPoint_iff_not_isBoundaryPoint`, `isInteriorPoint_iff_of_mem_atlas`, `isInteriorPoint_or_isBoundaryPoint`, `isOpen_interior`, `mem_interior_range_iff_of_mem_atlas`, `mem_interior_range_of_mem_interior_range_of_mem_atlas`, `range_mem_nhds_isInteriorPoint`	59
Total	64

BoundarylessManifold

Theorems

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

Diffeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`boundarylessManifold` 📖	mathematical	—	`BoundarylessManifold`	—	`IsLocalDiffeomorph.boundarylessManifold` `isLocalDiffeomorph`
`boundarylessManifold_iff` 📖	mathematical	—	`BoundarylessManifold`	—	`boundarylessManifold`
`image_boundary` 📖	mathematical	—	`Set.image` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike` `ModelWithCorners.boundary`	—	`Equiv.eq_preimage_iff_image_eq` `preimage_boundary`
`image_interior` 📖	mathematical	—	`Set.image` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike` `ModelWithCorners.interior`	—	`Equiv.eq_preimage_iff_image_eq` `preimage_interior`
`preimage_boundary` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike` `ModelWithCorners.boundary`	—	`IsLocalDiffeomorph.preimage_boundary` `isLocalDiffeomorph`
`preimage_interior` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike` `ModelWithCorners.interior`	—	`IsLocalDiffeomorph.preimage_interior` `isLocalDiffeomorph`

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_interior_convex_of_surjective_fderiv` 📖	mathematical	`DifferentiableAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Filter` `Filter.instMembership` `nhds` `Convex` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Set.Nonempty` `interior` `Set.MapsTo` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `fderiv`	`Set` `Set.instMembership` `interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `geometric_hahn_banach_open_point` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Convex.interior` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.instZeroLEOneClass` `isOpen_interior` `IsClosed.closure_eq` `closure_Iio` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `instNoMinOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `Convex.closure_interior_eq_closure_of_nonempty_interior` `Set.MapsTo.closure` `ContinuousLinearMap.continuous` `Filter.eventually_of_mem` `IsLocalMax.fderiv_eq_zero` `DFunLike.congr_fun` `RingHomCompTriple.ids` `ContinuousLinearMap.fderiv` `IsTopologicalAddGroup.toContinuousAdd` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `fderiv_comp` `ContinuousLinearMap.differentiableAt` `Mathlib.Tactic.Push.not_forall_eq` `ContinuousLinearMap.map_sub` `LT.lt.ne` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`

IsLocalDiffeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`boundarylessManifold` 📖	mathematical	`IsLocalDiffeomorph`	`BoundarylessManifold`	—	`preimage_boundary` `ModelWithCorners.Boundaryless.boundary_eq_empty`
`preimage_boundary` 📖	mathematical	`IsLocalDiffeomorph`	`Set.preimage` `ModelWithCorners.boundary`	—	`Set.inter_univ` `IsLocalDiffeomorphOn.preimage_boundary_inter` `isLocalDiffeomorphOn`
`preimage_interior` 📖	mathematical	`IsLocalDiffeomorph`	`Set.preimage` `ModelWithCorners.interior`	—	`Set.inter_univ` `IsLocalDiffeomorphOn.preimage_interior_inter` `isLocalDiffeomorphOn`

IsLocalDiffeomorphAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBoundaryPoint_iff` 📖	mathematical	`IsLocalDiffeomorphAt`	`ModelWithCorners.IsBoundaryPoint`	—	`isInteriorPoint_iff`
`isInteriorPoint_iff` 📖	mathematical	`IsLocalDiffeomorphAt`	`ModelWithCorners.IsInteriorPoint`	—	`MDifferentiableAt.isInteriorPoint_of_surjective_mfderiv` `mdifferentiableAt` `ContinuousLinearEquiv.surjective` `RingHomInvPair.ids` `localInverse_left_inv` `localInverse_mem_target` `localInverse_mdifferentiableAt`

IsLocalDiffeomorphOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preimage_boundary_inter` 📖	mathematical	`IsLocalDiffeomorphOn`	`Set` `Set.instInter` `Set.preimage` `ModelWithCorners.boundary`	—	`Set.ext` `IsLocalDiffeomorphAt.isBoundaryPoint_iff`
`preimage_interior_inter` 📖	mathematical	`IsLocalDiffeomorphOn`	`Set` `Set.instInter` `Set.preimage` `ModelWithCorners.interior`	—	`Set.ext` `IsLocalDiffeomorphAt.isInteriorPoint_iff`

MDifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isInteriorPoint_of_surjective_mfderiv` 📖	mathematical	`MDifferentiableAt` `TangentSpace` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.funLike` `mfderiv` `ModelWithCorners.IsInteriorPoint`	`ModelWithCorners.IsInteriorPoint`	—	`DifferentiableWithinAt.differentiableAt` `differentiableWithinAt_writtenInExtChartAt` `LinearMap.IsScalarTower.compatibleSMul` `Real.isScalarTower` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `DifferentiableAt.fderiv_restrictScalars` `ContinuousLinearMap.coe_restrictScalars'` `fderivWithin_eq_fderiv` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ModelWithCorners.uniqueDiffOn` `DifferentiableAt.restrictScalars` `DifferentiableAt.mem_interior_convex_of_surjective_fderiv` `Filter.inter_mem` `nhdsWithin_eq_nhds` `mem_interior_iff_mem_nhds` `extChartAt_target_mem_nhdsWithin` `extChartAt_preimage_mem_nhds` `ContinuousAt.preimage_mem_nhds` `continuousAt` `extChartAt_source_mem_nhds` `ModelWithCorners.convex_range` `ModelWithCorners.isClosed_range` `ModelWithCorners.nonempty_interior` `Set.MapsTo.mono_right` `writtenInExtChartAt_mapsTo` `extChartAt_target_subset_range` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv` `ModelWithCorners.range_eq_univ_of_not_isRCLikeNormedField` `interior_univ`

ModelWithCorners

Definitions

Name	Category	Theorems
`IsBoundaryPoint` 📖	MathDef	11 math math: `isInteriorPoint_or_isBoundaryPoint`, `Icc_isBoundaryPoint_bot`, `isBoundaryPoint_iff_not_isInteriorPoint`, `boundaryPoint_inl`, `isInteriorPoint_iff_not_isBoundaryPoint`, `isBoundaryPoint_iff_of_mem_atlas`, `boundaryPoint_inr`, `IsLocalDiffeomorphAt.isBoundaryPoint_iff`, `isBoundaryPoint_iff_isBoundaryPoint_val`, `isBoundaryPoint_iff`, `Icc_isBoundaryPoint_top`
`IsInteriorPoint` 📖	MathDef	15 math math: `isInteriorPoint_or_isBoundaryPoint`, `BoundarylessManifold.isInteriorPoint`, `isBoundaryPoint_iff_not_isInteriorPoint`, `Icc_isInteriorPoint_interior`, `isInteriorPoint_iff_isInteriorPoint_val`, `isInteriorPoint_iff_not_isBoundaryPoint`, `BoundarylessManifold.isInteriorPoint'`, `isInteriorPoint_iff`, `IsLocalDiffeomorphAt.isInteriorPoint_iff`, `isInteriorPoint_iff_of_mem_atlas`, `isInteriorPoint_disjointUnion_right`, `MDifferentiableAt.isInteriorPoint_of_surjective_mfderiv`, `isInteriorPoint_disjointUnion_left`, `interiorPoint_inl`, `interiorPoint_inr`
`boundary` 📖	CompOp	19 math math: `compl_boundary`, `instIsEmptyElemBoundaryOfBoundarylessManifold`, `Diffeomorph.image_boundary`, `interior_union_boundary_eq_univ`, `isClosed_boundary`, `boundary_open`, `Boundaryless.iff_boundary_eq_empty`, `boundary_disjointUnion`, `Boundaryless.boundary_eq_empty`, `compl_interior`, `boundary_of_boundaryless_left`, `IsLocalDiffeomorph.preimage_boundary`, `boundary_of_boundaryless_right`, `boundary_prod`, `disjoint_interior_boundary`, `IsLocalDiffeomorphOn.preimage_boundary_inter`, `boundary_Icc`, `Diffeomorph.preimage_boundary`, `boundary_product`
`interior` 📖	CompOp	13 math math: `compl_boundary`, `Diffeomorph.preimage_interior`, `interior_open`, `interior_eq_univ`, `interior_disjointUnion`, `interior_union_boundary_eq_univ`, `isOpen_interior`, `IsLocalDiffeomorphOn.preimage_interior_inter`, `compl_interior`, `IsLocalDiffeomorph.preimage_interior`, `Diffeomorph.image_interior`, `disjoint_interior_boundary`, `interior_prod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`boundaryPoint_inl` 📖	mathematical	`IsBoundaryPoint`	`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`	`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`	`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`	`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`
`isBoundaryPoint_iff_not_isInteriorPoint` 📖	mathematical	—	`IsBoundaryPoint` `IsInteriorPoint`	—	—
`isBoundaryPoint_iff_of_mem_atlas` 📖	mathematical	`OpenPartialHomeomorph` `Set` `Set.instMembership` `atlas` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	`IsBoundaryPoint` `Set` `Set.instMembership` `frontier` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.target` `OpenPartialHomeomorph.extend` `PartialEquiv.toFun`	—	`not_iff_not` `isInteriorPoint_iff_not_isBoundaryPoint` `isInteriorPoint_iff_of_mem_atlas` `mem_interior_iff_notMem_frontier` `PartialEquiv.mapsTo` `OpenPartialHomeomorph.extend_source`
`isClosed_boundary` 📖	mathematical	—	`IsClosed` `boundary`	—	`compl_interior` `isClosed_compl_iff` `isOpen_interior`
`isInteriorPoint_disjointUnion_left` 📖	mathematical	`IsInteriorPoint` `instTopologicalSpaceSum` `ChartedSpace.sum`	`IsInteriorPoint`	—	—
`isInteriorPoint_disjointUnion_right` 📖	mathematical	`IsInteriorPoint` `instTopologicalSpaceSum` `ChartedSpace.sum`	`IsInteriorPoint`	—	—
`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_iff_of_mem_atlas` 📖	mathematical	`OpenPartialHomeomorph` `Set` `Set.instMembership` `atlas` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	`IsInteriorPoint` `Set` `Set.instMembership` `interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.target` `OpenPartialHomeomorph.extend` `PartialEquiv.toFun`	—	`isInteriorPoint_iff` `mem_interior_range_iff_of_mem_atlas` `chart_mem_atlas` `mem_chart_source`
`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`
`isOpen_interior` 📖	mathematical	—	`IsOpen` `interior`	—	`isOpen_iff_forall_mem_open` `isInteriorPoint_iff_of_mem_atlas` `chart_mem_atlas` `isOpen_extChartAt_preimage` `isOpen_interior` `mem_chart_source` `isInteriorPoint_iff`
`mem_interior_range_iff_of_mem_atlas` 📖	mathematical	`OpenPartialHomeomorph` `Set` `Set.instMembership` `atlas` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	`Set` `Set.instMembership` `interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.target` `OpenPartialHomeomorph.extend` `PartialEquiv.toFun`	—	`mem_interior_range_of_mem_interior_range_of_mem_atlas`
`mem_interior_range_of_mem_interior_range_of_mem_atlas` 📖	mathematical	`OpenPartialHomeomorph` `Set` `Set.instMembership` `atlas` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.target` `OpenPartialHomeomorph.extend` `PartialEquiv.toFun`	`Set` `Set.instMembership` `interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.target` `OpenPartialHomeomorph.extend` `PartialEquiv.toFun`	—	`contDiffOn_extendCoordChange` `IsManifold.subset_maximalAtlas` `mem_interior_iff_mem_nhds` `OpenPartialHomeomorph.extend_source` `OpenPartialHomeomorph.extend_preimage_mem_nhds` `IsOpen.mem_nhds` `OpenPartialHomeomorph.open_source` `left_inv` `OpenPartialHomeomorph.left_inv` `DifferentiableOn.differentiableAt` `ContDiffOn.differentiableOn` `ContDiffOn.restrict_scalars` `Real.isScalarTower` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `DifferentiableAt.mem_interior_convex_of_surjective_fderiv` `convex_range` `isClosed_range` `nonempty_interior` `Set.MapsTo.mono_right` `PartialEquiv.mapsTo` `target_eq` `source_eq` `Set.inter_univ` `Set.inter_assoc` `fderivWithin_of_mem_nhds` `LinearMap.IsScalarTower.compatibleSMul` `DifferentiableWithinAt.restrictScalars_fderivWithin` `uniqueDiffWithinAt_of_mem_nhds` `Real.punctured_nhds_module_neBot` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Real.instNontrivial` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.coe_restrictScalars'` `range_eq_univ_of_not_isRCLikeNormedField` `interior_univ` `OpenPartialHomeomorph.mem_interior_extend_target` `PartialEquiv.restr_univ` `ContinuousLinearMap.IsInvertible.surjective` `isInvertible_fderivWithin_extendCoordChange`

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	12 math math: `ModelWithCorners.instBoundarylessManifold`, `ModelWithCorners.Boundaryless.of_boundary_eq_empty`, `ModelWithCorners.Boundaryless.iff_boundary_eq_empty`, `Diffeomorph.boundarylessManifold_iff`, `IsLocalDiffeomorph.boundarylessManifold`, `SingularManifold.boundaryless`, `SingularManifold.instBoundarylessManifoldRealM`, `ModelWithCorners.BoundarylessManifold.of_empty`, `ModelWithCorners.BoundarylessManifold.open`, `ModelWithCorners.boundaryless_disjointUnion`, `Diffeomorph.boundarylessManifold`, `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