eqToHom_hom₃ — Mathlib

English

Analogously, transporting along an equality preserves the third morphism component of the triangle morphism.

Русский

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

LaTeX

$$(eqToHom h)_{\text{hom},3} = 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

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