Theorems · Theorem · algebraic topology

SSet.prodStdSimplex.pairingCore.IsIndex.simplex_snd_succ

∀ {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 → (x.cast hd).simplex.2 l.succ = (x.cast hd).simplex.2 l.castSucc

Defined in: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
Cited by: 2 results in Mathlib
Foundations: Depth 68 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.

Cites18

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

DFunLike.coestatement · 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
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
SSet.boundarystatement and proof · cited by 141

Cited by2

Results whose statement or proof uses this declaration.

SSet.prodStdSimplex.pairingCore.IsType₂.type₁_eq_of_δ_eqproof · cited by 1
SSet.prodStdSimplex.pairingCore.IsIndex.eq_of_isType₂_δproof · cited by 0