Theorems · Inductive type · algebraic topology
SSet.Subcomplex.Pairing
{X : SSet} → X.Subcomplex → Type uA pairing for a subcomplex A of a simplicial set X consists of a partition
of the nondegenerate simplices of X not in A in two types (I) and (II) of simplices,
and a bijection between the type (II) simplices and the type (I) simplices.
See the introduction of the file
Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean.
- Cited by
- 117 results in Mathlib
- Foundations
- Depth 33 from the axioms, rests on 272 definitions · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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
Cited by190
Results whose statement or proof uses this declaration.
- SSet.Subcomplex.Pairing.RankFunctionstatement · cited by 68
- SSet.Subcomplex.Pairing.IIstatement and proof · cited by 58
- SSet.Subcomplex.Pairing.IsProperstatement · cited by 58
- SSet.Subcomplex.Pairing.RankFunction.Cellstatement · cited by 55
- SSet.Subcomplex.Pairing.RankFunction.Cell.dimstatement and proof · cited by 40
- SSet.Subcomplex.Pairing.RankFunction.filtrationstatement and proof · cited by 34
- SSet.Subcomplex.Pairing.pstatement and proof · cited by 32
- SSet.Subcomplex.Pairing.Istatement and proof · cited by 25
- SSet.Subcomplex.Pairing.AncestralRelstatement and proof · cited by 22
- SSet.Subcomplex.Pairing.RankFunction.sigmaStdSimplexstatement and proof · cited by 21
- SSet.Subcomplex.Pairing.RankFunction.Cell.sstatement and proof · cited by 21
- SSet.Subcomplex.Pairing.RankFunction.Cell.hornstatement and proof · cited by 19