existsUnique — Mathlib

English

Let k: W → X and h: k ≫ f = k ≫ g. Then there exists a unique l: W ⟶ equalizer f g with l ≫ equalizer.ι f g = k.

Русский

Пусть k: W → X и h: k ≫ f = k ≫ g. Тогда существует единственный l: W ⟶ equalizer f g такой, что l ≫ equalizer.ι f g = k.

LaTeX

$$$\exists! l:\, W \to \mathrm{equalizer}(f,g),\ l \circ \mathrm{equalizer.}\iota f g = k$$$

Lean4

theorem existsUnique {W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) : ∃! l : W ⟶ equalizer f g, l ≫ equalizer.ι f g = k :=
  Fork.IsLimit.existsUnique (limit.isLimit _) _ h

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