leftHomology_ext_iff — Mathlib

English

For any f1, f2 : S.leftHomology ⟶ A, f1 = f2 if and only if S.leftHomologyπ ≫ f1 = S.leftHomologyπ ≫ f2.

Русский

Для любых f1, f2 : S.leftHomology ⟶ A, f1 = f2 тогда и только тогда, когда S.leftHomologyπ ≫ f1 = S.leftHomologyπ ≫ f2.

LaTeX

$$$ f_1 = f_2 \\iff S.leftHomology\\pi \\gg f_1 = S.leftHomology\\pi \\gg f_2 $$$

Lean4

theorem leftHomology_ext_iff {A : C} (f₁ f₂ : S.leftHomology ⟶ A) :
    f₁ = f₂ ↔ S.leftHomologyπ ≫ f₁ = S.leftHomologyπ ≫ f₂ := by rw [cancel_epi]

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