coeq₃_condition₃ — Mathlib

English

For f,g,h: j1 → j2, we have f ≫ coeq₃Hom(f,g,h) = h ≫ coeq₃Hom(f,g,h).

Русский

Для f, g, h: j1 → j2 выполняется f ≫ coeq₃Hom(f,g,h) = h ≫ coeq₃Hom(f,g,h).

LaTeX

$$$\\forall {f g h : j_1 \\to j_2}, \\ f \\circ coeq₃Hom(f,g,h) = h \\circ coeq₃Hom(f,g,h).$$$

Lean4

theorem coeq₃_condition₃ {j₁ j₂ : C} (f g h : j₁ ⟶ j₂) : f ≫ coeq₃Hom f g h = h ≫ coeq₃Hom f g h :=
  Eq.trans (coeq₃_condition₁ f g h) (coeq₃_condition₂ f g h)

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