Mathlib Map

Theorems · Inductive type · algebraic topology

SSet.Subcomplex.Pairing.IsProper

{X : SSet} → {A : X.Subcomplex} → A.Pairing → Prop

A pairing is proper when each type (II) simplex is uniquely a 1-codimensional face of the corresponding (I) simplex.

Defined in
Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
Cited by
58 results in Mathlib
Foundations
Depth 34 from the axioms · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

SSet.Subcomplex.Pairing.RankFunction.Cell.horn · cited by 19Cell.hornSSet.Subcomplex.Pairing.RankFunction.sigmaHorn · cited by 18RankFunction.sigmaHornSSet.Subcomplex.Pairing.RankFunction.b · cited by 13RankFunction.bSSet.Subcomplex.Pairing.RankFunction.Cell.map · cited by 12Cell.mapSSet.Subcomplex.Pairing.RankFunction.m · cited by 12RankFunction.mSSet.Subcomplex.Pairing.isUniquelyCodimOneFace · cited by 12Pairing.isUniquelyCodimOn…SSet.Subcomplex.Pairing.RankFunction.Cell.index · cited by 10Cell.indexSSet.Subcomplex.Pairing.RankFunction.Cell.ιSigmaHorn · cited by 10Cell.ιSigmaHornSSet.Subcomplex.Pairing.RankFunction.Cell.mapToSucc · cited by 9Cell.mapToSuccSSet.Subcomplex.Pairing.RankFunction.t · cited by 9RankFunction.tSSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn · cited by 8Cell.mapHornSSet.Subcomplex.Pairing.IsInner · cited by 8Pairing.IsInnerSSet.Subcomplex.Pairing.RankFunction.Cell.type₁ · cited by 4Cell.type₁SSet.Subcomplex.Pairing.RankFunction.Cell.type₂ · cited by 4Cell.type₂SSet.Subcomplex.Pairing.RankFunction.mapN · cited by 4RankFunction.mapNSSet · cited by 1283SSetSSet.Subcomplex · cited by 461SSet.SubcomplexSSet.Subcomplex.Pairing · cited by 117Subcomplex.PairingPairing.IsProperCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by81

Results whose statement or proof uses this declaration.