Theorems · Theorem · algebraic topology

SSet.prodStdSimplex.pairingCore.IsIndex.succ_le_simplex_fst_iff

∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} {d : ℕ}
  {hd : x.dim = d} {l : Fin d},
  SSet.prodStdSimplex.pairingCore.IsIndex x hd l.succ →
    ∀ (i : Fin (d + 1)), k.succ ≤ (x.cast hd).simplex.1 i ↔ l.succ ≤ i

Defined in: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
Cited by: 2 results in Mathlib
Foundations: Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites22

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

DFunLike.coestatement and proof · cited by 62,936
CategoryTheory.Functor.objstatement · cited by 19,642
Oppositestatement · cited by 8,081
CategoryTheory.MonoidalCategoryStruct.tensorObjstatement · cited by 3,106
SimplexCategorystatement · cited by 2,204
SSetstatement · cited by 1,283
SSet.stdSimplexstatement · cited by 499
not_ltproof · cited by 306
SSet.N.toSstatement and proof · cited by 171
SSet.hornstatement and proof · cited by 162
SSet.S.dimstatement and proof · cited by 162
SSet.Subcomplex.Nstatement and proof · cited by 155

Cited by2

Results whose statement or proof uses this declaration.

SSet.prodStdSimplex.pairingCore.IsIndex.min_eqproof · cited by 3
SSet.prodStdSimplex.pairingCore.IsIndex.simplex_fst_le_castSucc_iffproof · cited by 0