const — Mathlib

English

There is a canonical degenerate subsimplex of Λ[n+2,i] concentrated at a fixed vertex k, giving a degenerate embedding into the horn.

Русский

Существуют канонические вырожденные подпростельные множества для Λ[n+2,i], концентрированные в вершине k, задающие вырожденное вложение в горн.

LaTeX

$$$ \text{const}(n,i) : Λ[n+2,i].obj \;m \; = \; SSet.yonedaEquiv( X := Λ[n+2,i] )( SSet.const( \langle stdSimplex.obj_0Equiv.symm k, \cdot \rangle ))$$$

Lean4

/-- The (degenerate) subsimplex of `Λ[n+2, i]` concentrated in vertex `k`. -/
def const (m : SimplexCategoryᵒᵖ) : Λ[n + 2, i].obj m :=
  SSet.yonedaEquiv (X := Λ[n + 2, i]) (SSet.const ⟨stdSimplex.obj₀Equiv.symm k, by simp⟩)

Похожие утверждения