app_two — Mathlib

English

On 2-simplices, mk.app outputs the two edge-mapped components forming a 2-simplex in the nerve.

Русский

На 2-симплексах mk.app выдает два реберных компонента, образующих 2-слой нервной структуры.

LaTeX

$$$\mathrm{mk.app}\;F\;⟦2⟧\;\varphi = \mathrm{mk}_2\big( F(\mathrm{ev}_{01}(\varphi)), F(\mathrm{ev}_{12}(\varphi))\big)$$$

Lean4

@[simp]
theorem app_two (φ : X _⦋2⦌₂) : mk.app F (⦋2⦌₂) φ = .mk₂ (F.map (ev01₂ φ)) (F.map (ev12₂ φ)) :=
  rfl

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