Documentation Verification Report

NonDegenerateSimplicesSubcomplex

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplicesSubcomplex.lean

Statistics

Metric	Count
Definitions `N`, `cast`, `instPartialOrder`, `mk`, `toN`	5
Theorems `cast_eq_self`, `ext_iff`, `le_iff`, `mk'_surjective`, `mk_dim`, `mk_simplex`, `mk_surjective`, `notMem`	8
Total	13

SSet.Subcomplex

Definitions

Name	Category	Theorems
`N` 📖	CompData	21 math math: `Pairing.instFiniteSubtypeElemNIIAncestralRel`, `Pairing.IsProper.isUniquelyCodimOneFace`, `PairingCore.injective_type₂`, `Pairing.dim_p`, `Pairing.isUniquelyCodimOneFace`, `Pairing.WeakRankFunction.wf_ancestralRel`, `Pairing.RankFunction.wf_ancestralRel`, `Pairing.IsRegular.wf`, `PairingCore.pairing_p_equivII`, `PairingCore.equivI_apply_coe`, `Pairing.AncestralRel.dim_le`, `N.le_iff`, `PairingCore.injective_type₁`, `Pairing.union`, `PairingCore.ancestralRel_iff`, `PairingCore.equivII_apply_coe`, `Pairing.instIsWellFoundedElemNIIAncestralRel`, `Pairing.wf`, `Pairing.exists_or`, `Pairing.inter`, `PairingCore.pairing_p_symm_equivI`

SSet.Subcomplex.N

Definitions

Name	Category	Theorems
`cast` 📖	CompOp	1 math math: `cast_eq_self`
`instPartialOrder` 📖	CompOp	1 math math: `le_iff`
`mk` 📖	CompOp	—
`toN` 📖	CompOp	18 math math: `SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace`, `SSet.Subcomplex.Pairing.IsProper.isUniquelyCodimOneFace`, `SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace_index`, `SSet.Subcomplex.Pairing.dim_p`, `SSet.Subcomplex.Pairing.isUniquelyCodimOneFace`, `SSet.Subcomplex.PairingCore.surjective'`, `SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace_index_coe`, `ext_iff`, `SSet.Subcomplex.PairingCore.type₂_dim`, `SSet.Subcomplex.PairingCore.type₂_simplex`, `SSet.Subcomplex.PairingCore.IsProper.isUniquelyCodimOneFace`, `SSet.Subcomplex.Pairing.AncestralRel.dim_le`, `le_iff`, `SSet.Subcomplex.PairingCore.type₁_dim`, `SSet.Subcomplex.PairingCore.type₁_simplex`, `mk_simplex`, `mk_dim`, `notMem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_eq_self` 📖	mathematical	`SSet.S.dim` `SSet.N.toS` `toN`	`cast`	—	—
`ext_iff` 📖	mathematical	—	`toN`	—	—
`le_iff` 📖	mathematical	—	`SSet.Subcomplex.N` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SSet.N` `SSet.N.instPreorder` `toN`	—	—
`mk'_surjective` 📖	mathematical	—	`mk'`	—	`notMem`
`mk_dim` 📖	mathematical	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `Set` `Set.instMembership` `SSet.nonDegenerate` `CategoryTheory.Subfunctor.obj`	`SSet.S.dim` `SSet.N.toS` `toN`	—	—
`mk_simplex` 📖	mathematical	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `Set` `Set.instMembership` `SSet.nonDegenerate` `CategoryTheory.Subfunctor.obj`	`SSet.S.simplex` `SSet.N.toS` `toN`	—	—
`mk_surjective` 📖	—	—	—	—	`SSet.N.nonDegenerate` `notMem`
`notMem` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `SSet.S.dim` `SSet.N.toS` `toN` `Set` `Set.instMembership` `CategoryTheory.Subfunctor.obj` `SSet.S.simplex`	—	—

---

← Back to Index