eqToHom_hom₂ — Mathlib

English

Similarly, equality-respecting transport preserves the second morphism component of the triangle morphism.

Русский

Аналогично: перенос по равенству сохраняет второй компонент гомоморфизма треугольника.

LaTeX

$$(eqToHom h)_{\text{hom},2} = eqToHom (by subst h; rfl)$$

Lean4

theorem eqToHom_hom₂ {A B : Triangle C} (h : A = B) : (eqToHom h).hom₂ = eqToHom (by subst h; rfl) := by subst h; rfl

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