equalizerSubobject_factors_iff — Mathlib

English

For h: W → X, h factors through equalizerSubobject f g if and only if h ≫ f = h ≫ g.

Русский

Для h: W → X факторизация через equalizerSubobject f g эквивалентна условию h ≫ f = h ≫ g.

LaTeX

$$$$ (equalizerSubobject f g).Factors h \\;\\Leftrightarrow\\; h \\gg f = h \\gg g $$$$

Lean4

theorem equalizerSubobject_factors_iff {W : C} (h : W ⟶ X) : (equalizerSubobject f g).Factors h ↔ h ≫ f = h ≫ g :=
  ⟨fun w => by rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, equalizerSubobject_arrow_comp, Category.assoc],
    equalizerSubobject_factors f g h⟩

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