Basic

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

Statistics

Metric	Count
Definitions SimplicialComplex, faces, facets, hasBot, instInhabited, instMin, instOrderBot, instSemilatticeInf, ofErase, ofSubcomplex, space, 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, isRelLowerSet_faces, 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	26
Total	38

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
faces 📖	CompOp	10 math math: mem_space_iff, ofErase_faces, vertices_eq, faces_bot, isRelLowerSet_faces, mem_facets, empty_notMem, mem_vertices, facets_subset, ext_iff
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
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 faces	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.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 faces	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.instSetLike space	—	Set.subset_biUnion_of_mem
disjoint_or_exists_inter_eq_convexHull 📖	mathematical	Finset Set Set.instMembership faces	Disjoint 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.instSetLike 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 📖	—	Finset Set Set.instMembership faces Finset.instHasSubset Finset.Nonempty	—	—	isRelLowerSet_faces
empty_notMem 📖	mathematical	—	Finset Set Set.instMembership faces Finset.instEmptyCollection	—	nonempty_of_mem_faces
ext 📖	—	faces	—	—	—
ext_iff 📖	mathematical	—	faces	—	ext
face_subset_face_iff 📖	mathematical	Finset Set Set.instMembership faces	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.instSetLike Finset.instHasSubset	—	vertex_mem_convexHull_iff down_closed Finset.singleton_subset_iff Finset.singleton_nonempty subset_convexHull convexHull_mono
faces_bot 📖	mathematical	—	faces 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 faces	—	—
indep 📖	mathematical	Finset Set Set.instMembership faces	AffineIndependent addGroupIsAddTorsor AddCommGroup.toAddGroup SetLike.instMembership Finset.instSetLike	—	—
inter_subset_convexHull 📖	mathematical	Finset Set Set.instMembership faces	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.instSetLike	—	—
isRelLowerSet_faces 📖	mathematical	—	IsRelLowerSet Finset Preorder.toLE PartialOrder.toPreorder Finset.partialOrder faces Finset.Nonempty	—	—
mem_facets 📖	mathematical	—	Finset Set Set.instMembership facets faces	—	Set.mem_sep_iff
mem_space_iff 📖	mathematical	—	Set Set.instMembership space Finset faces 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 faces Finset.instSingleton	—	—
nonempty_of_mem_faces 📖	mathematical	Finset Set Set.instMembership faces	Finset.Nonempty	—	isRelLowerSet_faces
not_facet_iff_subface 📖	mathematical	Finset Set Set.instMembership faces	facets 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	faces ofErase Set.instSDiff Set.instSingletonSet Finset.instEmptyCollection	—	—
ofSubcomplex_faces 📖	mathematical	Set Finset Set.instHasSubset faces IsLowerSet Preorder.toLE PartialOrder.toPreorder Finset.partialOrder	ofSubcomplex	—	—
space_bot 📖	mathematical	—	space Bot.bot Geometry.SimplicialComplex hasBot Set Set.instEmptyCollection	—	Set.biUnion_empty
subset_space 📖	mathematical	Finset Set Set.instMembership faces	Set.instHasSubset SetLike.coe Finset.instSetLike space	—	HasSubset.Subset.trans Set.instIsTransSubset subset_convexHull convexHull_subset_space
vertex_mem_convexHull_iff 📖	mathematical	Set Set.instMembership vertices Finset faces	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 Finset.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 faces 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