existsUnique — Mathlib

English

Let s be a Fork f g with IsLimit s. For any W, any k: W → X with k ≫ f = k ≫ g, there exists a unique l: W → s.pt with l ≫ s.ι = k.

Русский

Пусть s — форк f g и IsLimit s. Для любого W и k: W → X с k ≫ f = k ≫ g существует единственный l: W → s.pt такой, что l ≫ s.ι = k.

LaTeX

$$$\forall W\, \forall k:\, W \to X,\ h:\, k \to f = k \to g \Rightarrow \exists! l:\, W \to s.pt,\ l \circ s.\iota = k$$$

Lean4

theorem existsUnique {s : Fork f g} (hs : IsLimit s) {W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) :
    ∃! l : W ⟶ s.pt, l ≫ Fork.ι s = k :=
  ⟨hs.lift <| Fork.ofι _ h, hs.fac _ _, fun _ hm =>
    Fork.IsLimit.hom_ext hs <| hm.symm ▸ (hs.fac (Fork.ofι _ h) WalkingParallelPair.zero).symm⟩

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