eqToHom_hom₁ — Mathlib

English

If two triangles A and B are equal, then transporting along the equality preserves the first morphism component of the corresponding triangle morphisms.

Русский

Если треугольники A и B равны, то перенос по равенству сохраняет первый компонент гомоморфизма треугольников.

LaTeX

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

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