ev1₂ — Mathlib

English

Let V be a 2-truncated simplicial set and φ a 2-simplex of V. Then the middle vertex of φ yields an element of the 2-truncation of V, i.e., ev1₂ φ ∈ OneTruncation₂ V.

Русский

Пусть V — 2-отрезанный симплициальный набор и φ — 2-угольник V. Тогда средняя вершина φ даёт элемент в 2-окраске V, т.е. ev1₂ φ ∈ OneTruncation₂ V.

LaTeX

$$$ev_{1,2}(\\varphi) \\in \\mathrm{OneTruncation}_2(V)$$$

Lean4

/-- The middle vertex of a 2-simplex in a 2-truncated simplicial set. -/
def ev1₂ {V : SSet.Truncated 2} (φ : V _⦋2⦌₂) : OneTruncation₂ V :=
  V.map ι1₂.op φ

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