hom_ext — Mathlib

English

Two morphisms between squares are equal provided their four component arrows are equal componentwise.

Русский

Два морфизма между квадратами равны, если их четыре компонентных отображения равны попарно.

LaTeX

$$$f_\\tau_1 = g_\\tau_1 \\;\\land\\; f_\\tau_2 = g_\\tau_2 \\;\\land\\; f_\\tau_3 = g_\\tau_3 \\;\\land\\; f_\\tau_4 = g_\\tau_4 \\Rightarrow f = g$$$

Lean4

@[ext]
theorem hom_ext {sq₁ sq₂ : Square C} {f g : sq₁ ⟶ sq₂} (h₁ : f.τ₁ = g.τ₁) (h₂ : f.τ₂ = g.τ₂) (h₃ : f.τ₃ = g.τ₃)
    (h₄ : f.τ₄ = g.τ₄) : f = g :=
  Hom.ext h₁ h₂ h₃ h₄

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