hom_ext — Mathlib

English

Let L and L′ be objects in Φ.LeftResolution X₂. Then two arrows φ₁, φ₂: L → L′ are equal whenever their underlying component φ₁.f and φ₂.f agree; i.e., φ₁.f = φ₂.f implies φ₁ = φ₂.

Русский

Пусть L и L′ — объекты в Φ.LeftResolution X₂. Тогда любые две стрелки φ₁, φ₂: L → L′ равны, если их базовые компоненты совпадают: φ₁.f = φ₂.f ⇒ φ₁ = φ₂.

LaTeX

$$$\forall {L,L' : \Phi.LeftResolution X_2} \forall {\phi_1, \phi_2 : L \to L'}\ (\phi_1.f = \phi_2.f) \Rightarrow \phi_1 = \phi_2$$$

Lean4

@[ext]
theorem hom_ext {L L' : Φ.LeftResolution X₂} {φ₁ φ₂ : L ⟶ L'} (h : φ₁.f = φ₂.f) : φ₁ = φ₂ :=
  Hom.ext h

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