Theorems · Definition · algebraic topology
SSet.S.IsUniquelyCodimOneFace.index
{X : SSet} → {x y : X.S} → x.IsUniquelyCodimOneFace y → {d : ℕ} → x.dim = d → Fin (d + 2)When a d-dimensional simplex x is a 1-codimensional face of y, this is
the only i : Fin (d + 2), such that X.δ i y = x (with an abuse of notation:
see δ_index and δ_eq_iff for well typed statements).
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SSetstatement and proof · cited by 1,283
- SSet.S.dimstatement and proof · cited by 162
- SSet.Sstatement and proof · cited by 69
- SSet.S.IsUniquelyCodimOneFacestatement and proof · cited by 19
Cited by18
Results whose statement or proof uses this declaration.
- SSet.Subcomplex.Pairing.RankFunction.Cell.indexproof · cited by 10
- SSet.S.IsUniquelyCodimOneFace.δ_indexstatement · cited by 7
- SSet.S.IsUniquelyCodimOneFace.δ_eq_iffstatement and proof · cited by 3
- SSet.Subcomplex.Pairing.RankFunction.Cell.subcomplex_not_le_image_hornproof · cited by 2
- SSet.Subcomplex.Pairing.innerAnodyneExtensionsproof · cited by 2
- SSet.S.IsUniquelyCodimOneFace.leproof · cited by 2
- SSet.S.IsUniquelyCodimOneFace.uniquestatement · cited by 1
- SSet.Subcomplex.Pairing.IsInner.ne_laststatement · cited by 1
- SSet.Subcomplex.Pairing.IsInner.ne_zerostatement · cited by 1
- SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace_indexstatement · cited by 1
- SSet.S.IsUniquelyCodimOneFace.index_of_isostatement and proof · cited by 1
- SSet.Subcomplex.Pairing.pairingCoreproof · cited by 0