Theorems · Theorem · algebraic topology

SSet.StrictSegal.spineToSimplex_vertex

∀ {X : SSet} (sx : X.StrictSegal) {n : ℕ} (i : Fin (n + 1)) (f : X.Path n),
  (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } i).op)) (sx.spineToSimplex f) =
    f.vertex i

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Cited by

3 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound