Basic

📁 Source: Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean

Statistics

Metric	Count
Definitions `SimplicialComplex`, `facets`, `hasBot`, `instInhabited`, `instMin`, `instOrderBot`, `instSemilatticeInf`, `ofErase`, `ofSubcomplex`, `space`, `toPreAbstractSimplicialComplex`, `vertices`	12
Theorems `convexHull_inter_convexHull`, `convexHull_subset_space`, `disjoint_or_exists_inter_eq_convexHull`, `down_closed`, `empty_notMem`, `ext`, `ext_iff`, `face_subset_face_iff`, `faces_bot`, `facets_bot`, `facets_subset`, `indep`, `inter_subset_convexHull`, `mem_facets`, `mem_space_iff`, `mem_vertices`, `nonempty_of_mem_faces`, `not_facet_iff_subface`, `ofErase_faces`, `ofSubcomplex_faces`, `space_bot`, `subset_space`, `vertex_mem_convexHull_iff`, `vertices_eq`, `vertices_subset_space`	25
Total	37

Geometry

Definitions

Name	Category	Theorems
`SimplicialComplex` 📖	CompData	3 math math: `SimplicialComplex.space_bot`, `SimplicialComplex.faces_bot`, `SimplicialComplex.facets_bot`

Geometry.SimplicialComplex

Definitions

Name	Category	Theorems
`facets` 📖	CompOp	4 math math: `mem_facets`, `facets_subset`, `not_facet_iff_subface`, `facets_bot`
`hasBot` 📖	CompOp	3 math math: `space_bot`, `faces_bot`, `facets_bot`
`instInhabited` 📖	CompOp	—
`instMin` 📖	CompOp	—
`instOrderBot` 📖	CompOp	—
`instSemilatticeInf` 📖	CompOp	—
`ofErase` 📖	CompOp	1 math math: `ofErase_faces`
`ofSubcomplex` 📖	CompOp	1 math math: `ofSubcomplex_faces`
`space` 📖	CompOp	5 math math: `convexHull_subset_space`, `mem_space_iff`, `subset_space`, `space_bot`, `vertices_subset_space`
`toPreAbstractSimplicialComplex` 📖	CompOp	13 math math: `mem_space_iff`, `ofErase_faces`, `vertices_eq`, `faces_bot`, `ofSubcomplex_faces`, `down_closed`, `disjoint_or_exists_inter_eq_convexHull`, `mem_facets`, `empty_notMem`, `mem_vertices`, `facets_subset`, `not_facet_iff_subface`, `ext_iff`
`vertices` 📖	CompOp	3 math math: `vertices_eq`, `mem_vertices`, `vertices_subset_space`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convexHull_inter_convexHull` 📖	mathematical	`Finset` `Set` `Set.instMembership` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex`	`Set` `Set.instInter` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `inter_subset_convexHull` `Set.subset_inter` `convexHull_mono` `Set.inter_subset_left` `Set.inter_subset_right`
`convexHull_subset_space` 📖	mathematical	`Finset` `Set` `Set.instMembership` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex`	`Set` `Set.instHasSubset` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.coe` `Finset` `Finset.instSetLike` `space`	—	`Set.subset_biUnion_of_mem`
`disjoint_or_exists_inter_eq_convexHull` 📖	mathematical	`Finset` `Set` `Set.instMembership` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `ClosureOperator.instFunLike` `convexHull` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.coe` `Finset` `Finset.instSetLike` `Set.instMembership` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex` `Set.instInter`	—	`Set.not_disjoint_iff_nonempty_inter` `Mathlib.Tactic.Push.not_and_eq` `down_closed` `Finset.inter_subset_left` `convexHull_nonempty_iff` `Set.Nonempty.mono` `inter_subset_convexHull` `Finset.coe_inter` `convexHull_inter_convexHull`
`down_closed` 📖	mathematical	`Finset` `Set` `Set.instMembership` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex` `Finset.instHasSubset` `Finset.Nonempty`	`Finset` `Set` `Set.instMembership` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex`	—	`PreAbstractSimplicialComplex.isRelLowerSet_faces`
`empty_notMem` 📖	mathematical	—	`Finset` `Set` `Set.instMembership` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex` `Finset.instEmptyCollection`	—	`nonempty_of_mem_faces`
`ext` 📖	—	`PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex`	—	—	—
`ext_iff` 📖	mathematical	—	`PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex`	—	`ext`
`face_subset_face_iff` 📖	mathematical	`Finset` `Set` `Set.instMembership` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex`	`Set` `Set.instHasSubset` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.instHasSubset`	—	`vertex_mem_convexHull_iff` `down_closed` `Finset.singleton_subset_iff` `Finset.singleton_nonempty` `subset_convexHull` `convexHull_mono`
`faces_bot` 📖	mathematical	—	`PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex` `Bot.bot` `Geometry.SimplicialComplex` `hasBot` `Set` `Finset` `Set.instEmptyCollection`	—	—
`facets_bot` 📖	mathematical	—	`facets` `Bot.bot` `Geometry.SimplicialComplex` `hasBot` `Set` `Finset` `Set.instEmptyCollection`	—	`Set.eq_empty_of_subset_empty` `facets_subset`
`facets_subset` 📖	mathematical	—	`Set` `Finset` `Set.instHasSubset` `facets` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex`	—	—
`indep` 📖	mathematical	`Finset` `Set` `Set.instMembership` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex`	`AffineIndependent` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Finset` `SetLike.instMembership` `Finset.instSetLike`	—	—
`inter_subset_convexHull` 📖	mathematical	`Finset` `Set` `Set.instMembership` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex`	`Set` `Set.instHasSubset` `Set.instInter` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.coe` `Finset` `Finset.instSetLike`	—	—
`mem_facets` 📖	mathematical	—	`Finset` `Set` `Set.instMembership` `facets` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex`	—	`Set.mem_sep_iff`
`mem_space_iff` 📖	mathematical	—	`Set` `Set.instMembership` `space` `Finset` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.coe` `Finset.instSetLike`	—	—
`mem_vertices` 📖	mathematical	—	`Set` `Set.instMembership` `vertices` `Finset` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex` `Finset.instSingleton`	—	—
`nonempty_of_mem_faces` 📖	mathematical	`Finset` `Set` `Set.instMembership` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex`	`Finset.Nonempty`	—	`PreAbstractSimplicialComplex.isRelLowerSet_faces`
`not_facet_iff_subface` 📖	mathematical	`Finset` `Set` `Set.instMembership` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex`	`Finset` `Set` `Set.instMembership` `facets` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex` `Finset.instHasSSubset`	—	`Mathlib.Tactic.Push.not_and_eq` `Mathlib.Tactic.Push.not_forall_eq` `Finset.Subset.antisymm` `Finset.Subset.refl`
`ofErase_faces` 📖	mathematical	`AffineIndependent` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Finset` `SetLike.instMembership` `Finset.instSetLike` `IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `Set` `Set.instHasSubset` `Set.instInter` `DFunLike.coe` `ClosureOperator` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.coe`	`PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex` `ofErase` `Set` `Finset` `Set.instSDiff` `Set.instSingletonSet` `Finset.instEmptyCollection`	—	—
`ofSubcomplex_faces` 📖	mathematical	`Set` `Finset` `Set.instHasSubset` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex` `IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder`	`PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex` `ofSubcomplex`	—	—
`space_bot` 📖	mathematical	—	`space` `Bot.bot` `Geometry.SimplicialComplex` `hasBot` `Set` `Set.instEmptyCollection`	—	`Set.biUnion_empty`
`subset_space` 📖	mathematical	`Finset` `Set` `Set.instMembership` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex`	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `space`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_convexHull` `convexHull_subset_space`
`vertex_mem_convexHull_iff` 📖	mathematical	`Set` `Set.instMembership` `vertices` `Finset` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex`	`Set` `Set.instMembership` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.coe` `Finset` `Finset.instSetLike` `SetLike.instMembership`	—	`inter_subset_convexHull` `Finset.coe_singleton` `convexHull_singleton` `convexHull_empty` `Finset.coe_empty` `Finset.disjoint_iff_inter_eq_empty` `Disjoint.symm` `Finset.disjoint_singleton_right` `Finset.coe_inter` `subset_convexHull`
`vertices_eq` 📖	mathematical	—	`vertices` `Set.iUnion` `Finset` `Set` `Set.instMembership` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex` `SetLike.coe` `Finset.instSetLike`	—	`Set.ext` `Set.mem_biUnion` `Finset.mem_coe` `Finset.mem_singleton_self` `Set.mem_iUnion₂` `down_closed` `Finset.singleton_subset_iff` `Finset.singleton_nonempty`
`vertices_subset_space` 📖	mathematical	—	`Set` `Set.instHasSubset` `vertices` `space`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Eq.subset` `Set.instReflSubset` `vertices_eq` `Set.iUnion₂_mono` `subset_convexHull`

---

← Back to Index