Theorems · Definition · algebraic topology

SSet.PtSimplex.MulStruct.mulOne

{X : SSet} →
  {n : ℕ} →
    {x : X.obj (Opposite.op { len := 0 })} →
      (f : X.PtSimplex n x) → (i : Fin n) → f.MulStruct SSet.RelativeMorphism.const f i

Given f : X.PtSimplex n x and i : Fin n (note that this implies n ≠ 0), this is the term in MulStruct f .const f i corresponding to stdSimplex.σ i.succ ≫ f.map.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Cited by

1 results in Mathlib

Foundations

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