Documentation Verification Report

NonDegenerateSimplices

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

Statistics

Metric	Count
Definitions `N`, `cast`, `instPartialOrder`, `instPreorder`, `mk`, `toS`, `toN`, `orderEmbeddingN`	8
Theorems `cast_eq_self`, `dim_le_of_le`, `dim_lt_of_lt`, `eq_iff`, `ext_iff`, `iSup_subcomplex_eq_top`, `le_iff`, `le_iff_exists_mono`, `mk'_surjective`, `mk_dim`, `mk_simplex`, `mk_surjective`, `nonDegenerate`, `subcomplex_injective`, `subcomplex_injective_iff`, `existsUnique_n`, `subcomplex_toN`, `toN_eq_iff`, `orderEmbeddingN_apply`	19
Total	27

SSet

Definitions

Name	Category	Theorems
`N` 📖	CompData	8 math math: `iSup_subcomplexOfSimplex_prod_eq_top`, `orderEmbeddingN_apply`, `N.le_iff_exists_mono`, `Subcomplex.N.le_iff`, `N.le_iff`, `N.iSup_subcomplex_eq_top`, `Finite.finite`, `S.existsUnique_n`
`orderEmbeddingN` 📖	CompOp	1 math math: `orderEmbeddingN_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`orderEmbeddingN_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `N` `Subcomplex` `Preorder.toLE` `N.instPreorder` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `RelEmbedding.instFunLike` `orderEmbeddingN` `S.subcomplex` `N.toS`	—	—

SSet.N

Definitions

Name	Category	Theorems
`cast` 📖	CompOp	1 math math: `cast_eq_self`
`instPartialOrder` 📖	CompOp	—
`instPreorder` 📖	CompOp	4 math math: `SSet.orderEmbeddingN_apply`, `le_iff_exists_mono`, `SSet.Subcomplex.N.le_iff`, `le_iff`
`mk` 📖	CompOp	—
`toS` 📖	CompOp	32 math math: `SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace`, `SSet.Subcomplex.Pairing.IsProper.isUniquelyCodimOneFace`, `SSet.iSup_subcomplexOfSimplex_prod_eq_top`, `SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace_index`, `SSet.Subcomplex.Pairing.dim_p`, `SSet.Subcomplex.Pairing.isUniquelyCodimOneFace`, `SSet.Subcomplex.PairingCore.surjective'`, `dim_le_of_le`, `SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace_index_coe`, `ext_iff`, `mk_dim`, `dim_lt_of_lt`, `SSet.Subcomplex.PairingCore.type₂_dim`, `SSet.orderEmbeddingN_apply`, `SSet.Subcomplex.PairingCore.type₂_simplex`, `le_iff_exists_mono`, `SSet.Subcomplex.PairingCore.IsProper.isUniquelyCodimOneFace`, `SSet.Subcomplex.Pairing.AncestralRel.dim_le`, `SSet.Subcomplex.PairingCore.type₁_dim`, `subcomplex_injective_iff`, `mk_simplex`, `le_iff`, `nonDegenerate`, `SSet.S.toN_eq_iff`, `eq_iff`, `SSet.Subcomplex.PairingCore.type₁_simplex`, `iSup_subcomplex_eq_top`, `SSet.S.subcomplex_toN`, `SSet.Subcomplex.N.mk_simplex`, `SSet.Subcomplex.N.mk_dim`, `SSet.Subcomplex.N.notMem`, `SSet.S.existsUnique_n`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_eq_self` 📖	mathematical	`SSet.S.dim` `toS`	`cast`	—	—
`dim_le_of_le` 📖	mathematical	`SSet.N` `Preorder.toLE` `instPreorder`	`SSet.S.dim` `toS`	—	`le_iff_exists_mono` `SimplexCategory.len_le_of_mono`
`dim_lt_of_lt` 📖	mathematical	`SSet.N` `Preorder.toLT` `instPreorder`	`SSet.S.dim` `toS`	—	`LE.le.lt_or_eq` `dim_le_of_le` `LT.lt.le` `le_iff_exists_mono` `Subtype.prop` `mk_surjective` `CategoryTheory.FunctorToTypes.map_id_apply` `SimplexCategory.eq_id_of_mono`
`eq_iff` 📖	mathematical	—	`SSet.S.subcomplex` `toS`	—	—
`ext_iff` 📖	mathematical	—	`toS`	—	—
`iSup_subcomplex_eq_top` 📖	mathematical	—	`iSup` `SSet.Subcomplex` `SSet.N` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `SSet.S.subcomplex` `toS` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`le_antisymm` `SSet.Subcomplex.iSup_ofSimplex_nonDegenerate_eq_top` `iSup_le_iff` `le_trans` `le_refl` `le_iSup`
`le_iff` 📖	mathematical	—	`SSet.N` `Preorder.toLE` `instPreorder` `SSet.Subcomplex` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `SSet.S.subcomplex` `toS`	—	—
`le_iff_exists_mono` 📖	mathematical	—	`SSet.N` `Preorder.toLE` `instPreorder` `CategoryTheory.Functor.map` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `SSet.S.dim` `toS` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SSet.S.simplex`	—	`SSet.mono_of_nonDegenerate` `nonDegenerate`
`mk'_surjective` 📖	mathematical	—	`mk'`	—	`nonDegenerate`
`mk_dim` 📖	mathematical	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `Set` `Set.instMembership` `SSet.nonDegenerate`	`SSet.S.dim` `toS`	—	—
`mk_simplex` 📖	mathematical	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `Set` `Set.instMembership` `SSet.nonDegenerate`	`SSet.S.simplex` `toS`	—	—
`mk_surjective` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `Set` `Set.instMembership` `SSet.nonDegenerate` `Subtype.prop`	—	`Subtype.prop` `nonDegenerate`
`nonDegenerate` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `SSet.S.dim` `toS` `Set` `Set.instMembership` `SSet.nonDegenerate` `SSet.S.simplex`	—	—
`subcomplex_injective` 📖	—	`SSet.S.subcomplex` `toS`	—	—	`le_antisymm` `le_iff` `le_refl`
`subcomplex_injective_iff` 📖	mathematical	—	`SSet.S.subcomplex` `toS`	—	`subcomplex_injective`

SSet.S

Definitions

Name	Category	Theorems
`toN` 📖	CompOp	2 math math: `toN_eq_iff`, `subcomplex_toN`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`existsUnique_n` 📖	mathematical	—	`ExistsUnique` `SSet.N` `SSet.Subcomplex` `subcomplex` `SSet.N.toS`	—	`existsUnique_of_exists_of_unique` `mk_surjective` `SSet.exists_nonDegenerate` `Subtype.prop` `le_antisymm` `CategoryTheory.isSplitEpi_of_epi` `SimplexCategory.instSplitEpiCategory` `CategoryTheory.mono_iff_injective` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.instIsSplitMonoMap` `CategoryTheory.instIsSplitMonoOppositeOpOfIsSplitEpi` `CategoryTheory.FunctorToTypes.map_comp_apply` `CategoryTheory.op_comp` `CategoryTheory.Category.assoc` `CategoryTheory.IsSplitEpi.id` `CategoryTheory.Category.comp_id` `SSet.N.subcomplex_injective`
`subcomplex_toN` 📖	mathematical	—	`subcomplex` `SSet.N.toS` `toN`	—	`ExistsUnique.exists` `existsUnique_n`
`toN_eq_iff` 📖	mathematical	—	`toN` `subcomplex` `SSet.N.toS`	—	`subcomplex_toN` `ExistsUnique.unique` `existsUnique_n`

---

← Back to Index