ofHoms_v — Mathlib

English

Evaluation of the v-component on the diagonal recovers the original family.

Русский

Значение компоненты v на диагонали восстанавливает исходное семейство.

LaTeX

$$$ (\\operatorname{ofHoms}(\\psi)).v(p,p;\\mathrm{add\\,zero}\,p) = \\psi(p) $$$

Lean4

@[simp]
theorem ofHoms_v (ψ : ∀ (p : ℤ), F.X p ⟶ G.X p) (p : ℤ) : (ofHoms ψ).v p p (add_zero p) = ψ p := by
  simp only [ofHoms, mk_v, eqToHom_refl, comp_id]

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