cycles_ext_iff — Mathlib

English

For morphisms f1, f2 : A ⟶ S.cycles, f1 = f2 if and only if f1 ≫ iCycles = f2 ≫ iCycles.

Русский

Для морфизмов f1, f2 : A ⟶ S.cycles, f1 = f2 тогда и только тогда, когда f1 ≫ iCycles = f2 ≫ iCycles.

LaTeX

$$$ f_1 = f_2 \\iff f_1 \\circ S.iCycles = f_2 \\circ S.iCycles $$$

Lean4

theorem cycles_ext_iff {A : C} (f₁ f₂ : A ⟶ S.cycles) : f₁ = f₂ ↔ f₁ ≫ S.iCycles = f₂ ≫ S.iCycles := by rw [cancel_mono]

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