coeq₃_condition₂ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem coeq₃_condition₂ {j₁ j₂ : C} (f g h : j₁ ⟶ j₂) : g ≫ coeq₃Hom f g h = h ≫ coeq₃Hom f g h :=
  by
  dsimp [coeq₃Hom]
  slice_lhs 2 4 => rw [← Category.assoc, coeq_condition _ _]
  slice_rhs 2 4 => rw [← Category.assoc, coeq_condition _ _]
  slice_lhs 1 3 => rw [← Category.assoc, coeq_condition _ _]
  simp only [Category.assoc]

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