Theorems · Theorem · algebraic topology

SSet.PtSimplex.comp_map_eq_const

∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (s : X.PtSimplex n x) {Y : SSet}
  (φ : Y ⟶ SSet.stdSimplex.obj { len := n }) [Y.HasDimensionLT n],
  CategoryTheory.CategoryStruct.comp φ s.map = SSet.const x

Defined in: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Cited by: 2 results in Mathlib
Foundations: Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: SSet.HasDimensionLT

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites28

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

Setstatement · cited by 53,352
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Functor.objstatement and proof · cited by 19,642
CategoryTheory.CategoryStruct.compstatement · cited by 17,999
Top.topproof · cited by 9,680
Oppositestatement · cited by 8,081
SimplexCategorystatement · cited by 2,204
SSetstatement and proof · cited by 1,283
CategoryTheory.IsIsoproof · cited by 1,156
SSet.stdSimplexstatement and proof · cited by 499
SSet.Subcomplexproof · cited by 461
SSet.Subcomplex.toSSetstatement · cited by 315

Cited by2

Results whose statement or proof uses this declaration.

SSet.PtSimplex.δ_mapproof · cited by 1
SSet.PtSimplex.comp_map_eq_const_assocproof · cited by 0