Theorems · Inductive type · algebraic topology
SSet.Subcomplex.Pairing.IsRegular
{X : SSet} → {A : X.Subcomplex} → A.Pairing → PropA proper pairing is regular when the ancestrality relation is well founded.
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 34 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SSetstatement · cited by 1,283
- SSet.Subcomplexstatement · cited by 461
- SSet.Subcomplex.Pairingstatement · cited by 117
Cited by23
Results whose statement or proof uses this declaration.
- SSet.strongAnodyneExtensionsproof · cited by 6
- SSet.strongInnerAnodyneExtensionsproof · cited by 5
- SSet.Subcomplex.PairingCore.isRegular_pairing_iffstatement and proof · cited by 4
- SSet.Subcomplex.Pairing.anodyneExtensionsstatement and proof · cited by 2
- SSet.Subcomplex.Pairing.innerAnodyneExtensionsstatement and proof · cited by 2
- SSet.Subcomplex.Pairing.RankFunction.isRegularstatement · cited by 2
- SSet.Subcomplex.Pairing.rankFunctionstatement and proof · cited by 2
- SSet.Subcomplex.Pairing.strongAnodyneExtensionsstatement and proof · cited by 2
- SSet.Subcomplex.Pairing.WeakRankFunction.isRegularstatement · cited by 2
- SSet.Subcomplex.Pairing.IsRegular.wfstatement and proof · cited by 1
- SSet.Subcomplex.Pairing.isRegular_iff_nonempty_rankFunctionstatement and proof · cited by 1
- SSet.Subcomplex.Pairing.isRegular_iff_nonempty_weakRankFunctionstatement and proof · cited by 1