face — Mathlib

English

The jth face of codimension 1 of the i-th horn Λ[n+1,i] is obtained by excluding the j-th vertex and mapping via the standard embedding.

Русский

j-ое лицо горна кодом 1 размерности Λ[n+1,i] получается вычеркиванием j-й вершины и отображением через стандартную вложенность.

LaTeX

$$$\mathrm{face} : (\Lambda[n+1,i])⦋n⦌ \to SSet$$$

Lean4

/-- The `j`th face of codimension `1` of the `i`-th horn. -/
def face {n : ℕ} (i j : Fin (n + 2)) (h : j ≠ i) : (Λ[n + 1, i] : SSet.{u}) _⦋n⦌ :=
  yonedaEquiv (Subpresheaf.lift (stdSimplex.δ j) (by simpa using face_le_horn _ _ h))

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