Documentation Verification Report

IsUniquelyCodimOneFace

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean

Statistics

Metric	Count
Definitions `IsUniquelyCodimOneFace`, `index`	2
Theorems `cast`, `dim_eq`, `existsUnique_δ_cast_simplex`, `iff`, `δ_eq_iff`, `δ_index`	6
Total	8

SSet.S

Definitions

Name	Category	Theorems
`IsUniquelyCodimOneFace` 📖	MathDef	5 math math: `SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace`, `SSet.Subcomplex.Pairing.IsProper.isUniquelyCodimOneFace`, `SSet.Subcomplex.Pairing.isUniquelyCodimOneFace`, `SSet.Subcomplex.PairingCore.IsProper.isUniquelyCodimOneFace`, `IsUniquelyCodimOneFace.iff`

SSet.S.IsUniquelyCodimOneFace

Definitions

Name	Category	Theorems
`index` 📖	CompOp	4 math math: `SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace_index`, `SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace_index_coe`, `δ_eq_iff`, `δ_index`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast` 📖	mathematical	`SSet.S.IsUniquelyCodimOneFace` `SSet.S.dim`	`SSet.S.cast` `dim_eq`	—	`dim_eq` `SSet.S.cast_eq_self`
`dim_eq` 📖	mathematical	`SSet.S.IsUniquelyCodimOneFace`	`SSet.S.dim`	—	—
`existsUnique_δ_cast_simplex` 📖	mathematical	`SSet.S.IsUniquelyCodimOneFace` `SSet.S.dim`	`ExistsUnique` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `CategoryTheory.SimplicialObject.δ` `SSet.S.simplex` `SSet.S.cast`	—	`dim_eq` `cast`
`iff` 📖	mathematical	—	`SSet.S.IsUniquelyCodimOneFace` `ExistsUnique` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `CategoryTheory.SimplicialObject.δ`	—	`SimplexCategory.eq_δ_of_mono` `SimplexCategory.δ_injective` `SimplexCategory.instMonoδ`
`δ_eq_iff` 📖	mathematical	`SSet.S.IsUniquelyCodimOneFace` `SSet.S.dim`	`CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `SSet.S.simplex` `SSet.S.cast` `index`	—	`ExistsUnique.unique` `existsUnique_δ_cast_simplex` `δ_index`
`δ_index` 📖	mathematical	`SSet.S.IsUniquelyCodimOneFace` `SSet.S.dim`	`CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `index` `SSet.S.simplex` `SSet.S.cast`	—	`ExistsUnique.exists` `existsUnique_δ_cast_simplex`

---

← Back to Index