ev02₂ — Mathlib

English

The arrow in the refl-Quiver OneTruncation₂ V from ev0₂ φ to ev2₂ φ is the edge δ1₂ on φ, i.e., ev02₂ φ.

Русский

Стрела в reflQuiver OneTruncation₂ V от ev0₂ φ к ev2₂ φ задаётся ребром δ1₂ на φ, то есть ev02₂ φ.

LaTeX

$$$ev02_2(\\varphi) : ev0_2(\\varphi) \\to ev2_2(\\varphi)$$$

Lean4

/-- The arrow in the ReflQuiver `OneTruncation₂ V` of a 2-truncated simplicial set arising from the
1st face of a 2-simplex. -/
def ev02₂ {V : SSet.Truncated 2} (φ : V _⦋2⦌₂) : ev0₂ φ ⟶ ev2₂ φ :=
  ⟨V.map δ1₂.op φ, map_map_of_eq V rfl, map_map_of_eq V rfl⟩

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