equalizerSubobject_factors — Mathlib

English

Let W be any object and h: W → X with w: h ≫ f = h ≫ g. Then h factors through the subobject equalizerSubobject f g via the map equalizer.lift h w.

Русский

Пусть W — произвольный объект, а h: W → X удовлетворяет w: h ≫ f = h ≫ g. Тогда h факторизуется через подобъект equalizerSubobject f g при помощи отображения equalizer.lift h w.

LaTeX

$$$$(equalizerSubobject f g).Factors h$$$$

Lean4

theorem equalizerSubobject_factors {W : C} (h : W ⟶ X) (w : h ≫ f = h ≫ g) : (equalizerSubobject f g).Factors h :=
  ⟨equalizer.lift h w, by simp⟩

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