Intrinsic

📁 Source: Mathlib/Analysis/Convex/Intrinsic.lean

Statistics

Metric	Count
Definitions `intrinsicClosure`, `intrinsicFrontier`, `intrinsicInterior`	3
Theorems `image_intrinsicClosure`, `image_intrinsicFrontier`, `image_intrinsicInterior`, `intrinsicClosure`, `intrinsicClosure`, `intrinsicClosure`, `intrinsicInterior`, `ofIntrinsicClosure`, `affineSpan_intrinsicClosure`, `closure_diff_intrinsicFrontier`, `closure_diff_intrinsicInterior`, `interior_subset_intrinsicInterior`, `intrinsicClosure_diff_intrinsicFrontier`, `intrinsicClosure_diff_intrinsicInterior`, `intrinsicClosure_empty`, `intrinsicClosure_eq_closure`, `intrinsicClosure_eq_closure_inter_affineSpan`, `intrinsicClosure_idem`, `intrinsicClosure_mono`, `intrinsicClosure_nonempty`, `intrinsicClosure_singleton`, `intrinsicClosure_subset_affineSpan`, `intrinsicClosure_subset_closure`, `intrinsicFrontier_empty`, `intrinsicFrontier_singleton`, `intrinsicFrontier_subset`, `intrinsicFrontier_subset_frontier`, `intrinsicFrontier_subset_intrinsicClosure`, `intrinsicFrontier_union_intrinsicInterior`, `intrinsicInterior_empty`, `intrinsicInterior_nonempty`, `intrinsicInterior_singleton`, `intrinsicInterior_subset`, `intrinsicInterior_union_intrinsicFrontier`, `isClosed_intrinsicClosure`, `isClosed_intrinsicFrontier`, `mem_intrinsicClosure`, `mem_intrinsicFrontier`, `mem_intrinsicInterior`, `subset_intrinsicClosure`	40
Total	43

AffineIsometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_intrinsicClosure` 📖	mathematical	—	`intrinsicClosure` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NormedAddTorsor.toAddTorsor` `Set.image` `DFunLike.coe` `AffineIsometry` `MetricSpace.toPseudoMetricSpace` `instFunLike`	—	`Set.eq_empty_or_nonempty` `Set.image_empty` `intrinsicClosure_empty` `IsScalarTower.left` `instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `Set.Nonempty.to_subtype` `AffineSubspace.nonempty_map` `AffineSubspace.isometryEquivMap.apply_symm_apply` `intrinsicClosure.eq_1` `coe_toAffineMap` `AffineSubspace.map_span` `Function.comp_assoc` `Set.image_comp` `Homeomorph.image_closure` `Homeomorph.image_symm` `Set.preimage_comp` `Homeomorph.symm_comp_self` `Function.Injective.preimage_image` `injective`
`image_intrinsicFrontier` 📖	mathematical	—	`intrinsicFrontier` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NormedAddTorsor.toAddTorsor` `Set.image` `DFunLike.coe` `AffineIsometry` `MetricSpace.toPseudoMetricSpace` `instFunLike`	—	`Set.eq_empty_or_nonempty` `Set.image_empty` `intrinsicFrontier_empty` `IsScalarTower.left` `instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `Set.Nonempty.to_subtype` `AffineSubspace.nonempty_map` `AffineSubspace.isometryEquivMap.apply_symm_apply` `intrinsicFrontier.eq_1` `coe_toAffineMap` `AffineSubspace.map_span` `Function.comp_assoc` `Set.image_comp` `Homeomorph.image_frontier` `Homeomorph.image_symm` `Set.preimage_comp` `Homeomorph.symm_comp_self` `Function.Injective.preimage_image` `injective`
`image_intrinsicInterior` 📖	mathematical	—	`intrinsicInterior` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NormedAddTorsor.toAddTorsor` `Set.image` `DFunLike.coe` `AffineIsometry` `MetricSpace.toPseudoMetricSpace` `instFunLike`	—	`Set.eq_empty_or_nonempty` `Set.image_empty` `intrinsicInterior_empty` `IsScalarTower.left` `instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `Set.Nonempty.to_subtype` `AffineSubspace.nonempty_map` `AffineSubspace.isometryEquivMap.apply_symm_apply` `intrinsicInterior.eq_1` `coe_toAffineMap` `AffineSubspace.map_span` `Function.comp_assoc` `Set.image_comp` `Homeomorph.image_interior` `Homeomorph.image_symm` `Set.preimage_comp` `Homeomorph.symm_comp_self` `Function.Injective.preimage_image` `injective`

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intrinsicClosure` 📖	mathematical	`Convex` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`Convex` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `intrinsicClosure` `DivisionRing.toRing` `Field.toDivisionRing` `addGroupIsAddTorsor`	—	`intrinsicClosure_eq_closure_inter_affineSpan` `inter` `closure` `AffineSubspace.convex`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intrinsicClosure` 📖	mathematical	—	`intrinsicClosure`	—	`intrinsicClosure.eq_1` `closure_eq` `Set.image_preimage_eq_of_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_affineSpan` `Eq.superset` `Set.instReflSubset` `Subtype.range_coe`

Set.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intrinsicClosure` 📖	mathematical	`Set.Nonempty`	`Set.Nonempty` `intrinsicClosure`	—	`intrinsicClosure_nonempty`
`intrinsicInterior` 📖	mathematical	`Convex` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Set.Nonempty`	`Set.Nonempty` `intrinsicInterior` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `SeminormedAddCommGroup.toNormedAddTorsor`	—	`subset_affineSpan` `intrinsicInterior.eq_1` `Set.image_nonempty` `IsScalarTower.left` `instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `coe_sort` `Convex.interior_nonempty_iff_affineSpan_eq_top` `FiniteDimensional.finiteDimensional_submodule` `Convex.affine_preimage` `AffineIsometryEquiv.coe_toHomeomorph` `AffineIsometryEquiv.coe_toAffineEquiv` `AffineSubspace.comap_span` `affineSpan_coe_preimage_eq_top` `AffineSubspace.comap_top`
`ofIntrinsicClosure` 📖	mathematical	`Set.Nonempty` `intrinsicClosure`	`Set.Nonempty`	—	`intrinsicClosure_nonempty`

(root)

Definitions

Name	Category	Theorems
`intrinsicClosure` 📖	CompOp	22 math math: `AffineIsometry.image_intrinsicClosure`, `intrinsicClosure_diff_intrinsicFrontier`, `Convex.intrinsicClosure`, `subset_intrinsicClosure`, `intrinsicClosure_singleton`, `isClosed_intrinsicClosure`, `intrinsicInterior_union_intrinsicFrontier`, `Set.Nonempty.intrinsicClosure`, `intrinsicClosure_mono`, `intrinsicClosure_idem`, `intrinsicClosure_eq_closure_inter_affineSpan`, `intrinsicClosure_diff_intrinsicInterior`, `IsClosed.intrinsicClosure`, `affineSpan_intrinsicClosure`, `intrinsicFrontier_union_intrinsicInterior`, `intrinsicClosure_empty`, `intrinsicClosure_nonempty`, `intrinsicClosure_eq_closure`, `intrinsicClosure_subset_closure`, `intrinsicClosure_subset_affineSpan`, `mem_intrinsicClosure`, `intrinsicFrontier_subset_intrinsicClosure`
`intrinsicFrontier` 📖	CompOp	14 math math: `closure_diff_intrinsicFrontier`, `intrinsicClosure_diff_intrinsicFrontier`, `mem_intrinsicFrontier`, `intrinsicFrontier_subset_frontier`, `intrinsicInterior_union_intrinsicFrontier`, `intrinsicFrontier_empty`, `intrinsicFrontier_subset`, `isClosed_intrinsicFrontier`, `intrinsicClosure_diff_intrinsicInterior`, `intrinsicFrontier_union_intrinsicInterior`, `intrinsicFrontier_singleton`, `closure_diff_intrinsicInterior`, `AffineIsometry.image_intrinsicFrontier`, `intrinsicFrontier_subset_intrinsicClosure`
`intrinsicInterior` 📖	CompOp	14 math math: `closure_diff_intrinsicFrontier`, `intrinsicClosure_diff_intrinsicFrontier`, `interior_subset_intrinsicInterior`, `intrinsicInterior_subset`, `Set.Nonempty.intrinsicInterior`, `AffineIsometry.image_intrinsicInterior`, `intrinsicInterior_union_intrinsicFrontier`, `intrinsicInterior_empty`, `intrinsicClosure_diff_intrinsicInterior`, `intrinsicInterior_nonempty`, `intrinsicFrontier_union_intrinsicInterior`, `closure_diff_intrinsicInterior`, `intrinsicInterior_singleton`, `mem_intrinsicInterior`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affineSpan_intrinsicClosure` 📖	mathematical	—	`affineSpan` `intrinsicClosure`	—	`LE.le.antisymm` `affineSpan_le` `intrinsicClosure_subset_affineSpan` `affineSpan_mono` `subset_intrinsicClosure`
`closure_diff_intrinsicFrontier` 📖	mathematical	—	`Set` `Set.instSDiff` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `intrinsicFrontier` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `intrinsicInterior`	—	`intrinsicClosure_diff_intrinsicFrontier` `intrinsicClosure_eq_closure`
`closure_diff_intrinsicInterior` 📖	mathematical	—	`Set` `Set.instSDiff` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `intrinsicInterior` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `intrinsicFrontier`	—	`intrinsicClosure_diff_intrinsicInterior` `intrinsicClosure_eq_closure`
`interior_subset_intrinsicInterior` 📖	mathematical	—	`Set` `Set.instHasSubset` `interior` `intrinsicInterior`	—	`subset_affineSpan` `interior_subset` `preimage_interior_subset_interior_preimage` `continuous_subtype_val`
`intrinsicClosure_diff_intrinsicFrontier` 📖	mathematical	—	`Set` `Set.instSDiff` `intrinsicClosure` `intrinsicFrontier` `intrinsicInterior`	—	`Set.image_diff` `Subtype.coe_injective` `closure_diff_frontier` `intrinsicInterior.eq_1`
`intrinsicClosure_diff_intrinsicInterior` 📖	mathematical	—	`Set` `Set.instSDiff` `intrinsicClosure` `intrinsicInterior` `intrinsicFrontier`	—	`Set.image_diff` `Subtype.coe_injective`
`intrinsicClosure_empty` 📖	mathematical	—	`intrinsicClosure` `Set` `Set.instEmptyCollection`	—	`IsClosed.closure_eq` `Set.image_empty`
`intrinsicClosure_eq_closure` 📖	mathematical	—	`intrinsicClosure` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `closure`	—	`Set.ext` `Continuous.isOpen_preimage` `continuous_induced_dom` `IsClosed.isOpen_compl` `AffineSubspace.closed_of_finiteDimensional` `FiniteDimensional.finiteDimensional_submodule` `subset_affineSpan`
`intrinsicClosure_eq_closure_inter_affineSpan` 📖	mathematical	—	`intrinsicClosure` `Set` `Set.instInter` `closure` `SetLike.coe` `AffineSubspace` `AffineSubspace.instSetLike` `affineSpan`	—	`Topology.IsInducing.subtypeVal` `intrinsicClosure.eq_1` `Topology.IsInducing.closure_eq_preimage_closure_image` `Set.image_preimage_eq_inter_range` `Set.image_preimage_eq_of_subset` `Subtype.range_coe` `subset_affineSpan`
`intrinsicClosure_idem` 📖	mathematical	—	`intrinsicClosure`	—	`IsClosed.intrinsicClosure` `intrinsicClosure.eq_1` `Set.preimage_image_eq` `Subtype.coe_injective` `isClosed_closure` `affineSpan_intrinsicClosure`
`intrinsicClosure_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`Set` `Set.instHasSubset` `intrinsicClosure`	—	`Set.image_subset_iff` `affineSpan_mono` `Continuous.closure_preimage_subset` `continuous_inclusion` `closure_mono`
`intrinsicClosure_nonempty` 📖	mathematical	—	`Set.Nonempty` `intrinsicClosure`	—	`intrinsicClosure_empty` `Set.Nonempty.mono` `subset_intrinsicClosure`
`intrinsicClosure_singleton` 📖	mathematical	—	`intrinsicClosure` `Set` `Set.instSingletonSet`	—	`AffineSubspace.preimage_coe_affineSpan_singleton` `closure_univ` `Set.image_univ` `Subtype.range_coe_subtype`
`intrinsicClosure_subset_affineSpan` 📖	mathematical	—	`Set` `Set.instHasSubset` `intrinsicClosure` `SetLike.coe` `AffineSubspace` `AffineSubspace.instSetLike` `affineSpan`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.image_subset_range` `Eq.subset` `Set.instReflSubset` `Subtype.range_coe`
`intrinsicClosure_subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `intrinsicClosure` `closure`	—	`Set.image_subset_iff` `Continuous.closure_preimage_subset` `continuous_subtype_val`
`intrinsicFrontier_empty` 📖	mathematical	—	`intrinsicFrontier` `Set` `Set.instEmptyCollection`	—	`frontier_empty` `Set.image_empty`
`intrinsicFrontier_singleton` 📖	mathematical	—	`intrinsicFrontier` `Set` `Set.instSingletonSet` `Set.instEmptyCollection`	—	`intrinsicFrontier.eq_1` `AffineSubspace.preimage_coe_affineSpan_singleton` `frontier_univ` `Set.image_empty`
`intrinsicFrontier_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `intrinsicFrontier`	—	`Set.image_subset_iff` `IsClosed.frontier_subset` `IsClosed.preimage` `continuous_induced_dom`
`intrinsicFrontier_subset_frontier` 📖	mathematical	—	`Set` `Set.instHasSubset` `intrinsicFrontier` `frontier`	—	`Set.image_subset_iff` `Continuous.frontier_preimage_subset` `continuous_subtype_val`
`intrinsicFrontier_subset_intrinsicClosure` 📖	mathematical	—	`Set` `Set.instHasSubset` `intrinsicFrontier` `intrinsicClosure`	—	`Set.image_mono` `frontier_subset_closure`
`intrinsicFrontier_union_intrinsicInterior` 📖	mathematical	—	`Set` `Set.instUnion` `intrinsicFrontier` `intrinsicInterior` `intrinsicClosure`	—	`Set.union_comm` `intrinsicInterior_union_intrinsicFrontier`
`intrinsicInterior_empty` 📖	mathematical	—	`intrinsicInterior` `Set` `Set.instEmptyCollection`	—	`interior_empty` `Set.image_empty`
`intrinsicInterior_nonempty` 📖	mathematical	`Convex` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField`	`Set.Nonempty` `intrinsicInterior` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `SeminormedAddCommGroup.toNormedAddTorsor`	—	`intrinsicInterior_empty` `Set.Nonempty.intrinsicInterior`
`intrinsicInterior_singleton` 📖	mathematical	—	`intrinsicInterior` `Set` `Set.instSingletonSet`	—	`AffineSubspace.preimage_coe_affineSpan_singleton` `interior_univ` `Set.image_univ` `Subtype.range_coe_subtype`
`intrinsicInterior_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `intrinsicInterior`	—	`Set.image_subset_iff` `interior_subset`
`intrinsicInterior_union_intrinsicFrontier` 📖	mathematical	—	`Set` `Set.instUnion` `intrinsicInterior` `intrinsicFrontier` `intrinsicClosure`	—	`closure_eq_interior_union_frontier` `Set.image_union`
`isClosed_intrinsicClosure` 📖	mathematical	—	`IsClosed` `intrinsicClosure`	—	`Topology.IsClosedEmbedding.isClosedMap` `IsClosed.isClosedEmbedding_subtypeVal` `isClosed_closure`
`isClosed_intrinsicFrontier` 📖	mathematical	—	`IsClosed` `intrinsicFrontier`	—	`Topology.IsClosedEmbedding.isClosedMap` `IsClosed.isClosedEmbedding_subtypeVal` `isClosed_frontier`
`mem_intrinsicClosure` 📖	mathematical	—	`Set` `Set.instMembership` `intrinsicClosure` `AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `closure` `instTopologicalSpaceSubtype` `Set.preimage`	—	`Set.mem_image`
`mem_intrinsicFrontier` 📖	mathematical	—	`Set` `Set.instMembership` `intrinsicFrontier` `AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `frontier` `instTopologicalSpaceSubtype` `Set.preimage`	—	`Set.mem_image`
`mem_intrinsicInterior` 📖	mathematical	—	`Set` `Set.instMembership` `intrinsicInterior` `AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `interior` `instTopologicalSpaceSubtype` `Set.preimage`	—	`Set.mem_image`
`subset_intrinsicClosure` 📖	mathematical	—	`Set` `Set.instHasSubset` `intrinsicClosure`	—	`subset_affineSpan` `subset_closure`

---

← Back to Index