Documentation Verification Report

Basic

📁 Source: Mathlib/AlgebraicTopology/SimplicialComplex/Basic.lean

Statistics

Metric	Count
Definitions `AbstractSimplicialComplex`, `instBot`, `instCompleteLattice`, `instCompleteSemilatticeInf`, `instCompleteSemilatticeSup`, `instInfSet`, `instLE`, `instLT`, `instMax`, `instMin`, `instPartialOrder`, `instSetLikeFinset`, `instSupSet`, `instTop`, `toPreAbstractSimplicialComplex`, `PreAbstractSimplicialComplex`, `addSingletons`, `faces`, `instBot`, `instCompleteLattice`, `instCompleteSemilatticeInf`, `instCompleteSemilatticeSup`, `instInfSet`, `instLE`, `instLT`, `instMax`, `instMin`, `instPartialOrder`, `instSetLikeFinset`, `instSupSet`, `instTop`, `map`, `toAbstractSimplicialComplex`	33
Theorems `ext`, `ext_iff`, `instIsConcreteLEFinset`, `singleton_mem`, `toPreAbstractSimplicialComplex_injective`, `toPreAbstractSimplicialComplex_le_iff`, `toPreAbstractSimplicialComplex_lt_iff`, `top_toPreAbstractSimplicialComplex`, `ext`, `ext_iff`, `instIsConcreteLEFinset`, `isRelLowerSet_faces`	12
Total	45

AbstractSimplicialComplex

Definitions

Name	Category	Theorems
`instBot` 📖	CompOp	—
`instCompleteLattice` 📖	CompOp	—
`instCompleteSemilatticeInf` 📖	CompOp	—
`instCompleteSemilatticeSup` 📖	CompOp	—
`instInfSet` 📖	CompOp	—
`instLE` 📖	CompOp	2 math math: `toPreAbstractSimplicialComplex_le_iff`, `instIsConcreteLEFinset`
`instLT` 📖	CompOp	1 math math: `toPreAbstractSimplicialComplex_lt_iff`
`instMax` 📖	CompOp	—
`instMin` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	—
`instSetLikeFinset` 📖	CompOp	1 math math: `instIsConcreteLEFinset`
`instSupSet` 📖	CompOp	—
`instTop` 📖	CompOp	1 math math: `top_toPreAbstractSimplicialComplex`
`toPreAbstractSimplicialComplex` 📖	CompOp	6 math math: `toPreAbstractSimplicialComplex_lt_iff`, `toPreAbstractSimplicialComplex_le_iff`, `ext_iff`, `top_toPreAbstractSimplicialComplex`, `singleton_mem`, `toPreAbstractSimplicialComplex_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex`	—	—	—
`ext_iff` 📖	mathematical	—	`PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex`	—	`ext`
`instIsConcreteLEFinset` 📖	mathematical	—	`IsConcreteLE` `AbstractSimplicialComplex` `Finset` `instSetLikeFinset` `instLE`	—	—
`singleton_mem` 📖	mathematical	—	`Finset` `Set` `Set.instMembership` `PreAbstractSimplicialComplex.faces` `toPreAbstractSimplicialComplex` `Finset.instSingleton`	—	—
`toPreAbstractSimplicialComplex_injective` 📖	mathematical	—	`AbstractSimplicialComplex` `PreAbstractSimplicialComplex` `toPreAbstractSimplicialComplex`	—	`ext`
`toPreAbstractSimplicialComplex_le_iff` 📖	mathematical	—	`PreAbstractSimplicialComplex` `PreAbstractSimplicialComplex.instLE` `toPreAbstractSimplicialComplex` `AbstractSimplicialComplex` `instLE`	—	—
`toPreAbstractSimplicialComplex_lt_iff` 📖	mathematical	—	`PreAbstractSimplicialComplex` `PreAbstractSimplicialComplex.instLT` `toPreAbstractSimplicialComplex` `AbstractSimplicialComplex` `instLT`	—	—
`top_toPreAbstractSimplicialComplex` 📖	mathematical	—	`toPreAbstractSimplicialComplex` `Top.top` `AbstractSimplicialComplex` `instTop` `PreAbstractSimplicialComplex` `PreAbstractSimplicialComplex.instTop`	—	—

PreAbstractSimplicialComplex

Definitions

Name	Category	Theorems
`addSingletons` 📖	CompOp	—
`faces` 📖	CompOp	17 math math: `Geometry.SimplicialComplex.mem_space_iff`, `Geometry.SimplicialComplex.ofErase_faces`, `Geometry.SimplicialComplex.vertices_eq`, `Geometry.SimplicialComplex.faces_bot`, `Geometry.SimplicialComplex.ofSubcomplex_faces`, `Geometry.SimplicialComplex.down_closed`, `Geometry.SimplicialComplex.disjoint_or_exists_inter_eq_convexHull`, `Geometry.SimplicialComplex.mem_facets`, `Geometry.SimplicialComplex.empty_notMem`, `AbstractSimplicialComplex.ext_iff`, `Geometry.SimplicialComplex.mem_vertices`, `isRelLowerSet_faces`, `ext_iff`, `Geometry.SimplicialComplex.facets_subset`, `AbstractSimplicialComplex.singleton_mem`, `Geometry.SimplicialComplex.not_facet_iff_subface`, `Geometry.SimplicialComplex.ext_iff`
`instBot` 📖	CompOp	—
`instCompleteLattice` 📖	CompOp	—
`instCompleteSemilatticeInf` 📖	CompOp	—
`instCompleteSemilatticeSup` 📖	CompOp	—
`instInfSet` 📖	CompOp	—
`instLE` 📖	CompOp	2 math math: `AbstractSimplicialComplex.toPreAbstractSimplicialComplex_le_iff`, `instIsConcreteLEFinset`
`instLT` 📖	CompOp	1 math math: `AbstractSimplicialComplex.toPreAbstractSimplicialComplex_lt_iff`
`instMax` 📖	CompOp	—
`instMin` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	—
`instSetLikeFinset` 📖	CompOp	1 math math: `instIsConcreteLEFinset`
`instSupSet` 📖	CompOp	—
`instTop` 📖	CompOp	1 math math: `AbstractSimplicialComplex.top_toPreAbstractSimplicialComplex`
`map` 📖	CompOp	—
`toAbstractSimplicialComplex` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`faces`	—	—	—
`ext_iff` 📖	mathematical	—	`faces`	—	`ext`
`instIsConcreteLEFinset` 📖	mathematical	—	`IsConcreteLE` `PreAbstractSimplicialComplex` `Finset` `instSetLikeFinset` `instLE`	—	—
`isRelLowerSet_faces` 📖	mathematical	—	`IsRelLowerSet` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `faces` `Finset.Nonempty`	—	—

(root)

Definitions

Name	Category	Theorems
`AbstractSimplicialComplex` 📖	CompData	5 math math: `AbstractSimplicialComplex.toPreAbstractSimplicialComplex_lt_iff`, `AbstractSimplicialComplex.toPreAbstractSimplicialComplex_le_iff`, `AbstractSimplicialComplex.instIsConcreteLEFinset`, `AbstractSimplicialComplex.top_toPreAbstractSimplicialComplex`, `AbstractSimplicialComplex.toPreAbstractSimplicialComplex_injective`
`PreAbstractSimplicialComplex` 📖	CompData	5 math math: `AbstractSimplicialComplex.toPreAbstractSimplicialComplex_lt_iff`, `AbstractSimplicialComplex.toPreAbstractSimplicialComplex_le_iff`, `PreAbstractSimplicialComplex.instIsConcreteLEFinset`, `AbstractSimplicialComplex.top_toPreAbstractSimplicialComplex`, `AbstractSimplicialComplex.toPreAbstractSimplicialComplex_injective`

---

← Back to Index