lift_snd — Mathlib

English

Let t be a PullbackCone for f: X → Z and g: Y → Z, ht an IsLimit. For h: W → X, k: W → Y, and w: h ≫ f = k ≫ g, the universal arrow IsLimit.lift ht h k w satisfies (IsLimit.lift ht h k w) ≫ snd t = k.

Русский

Пусть t — пуллбэк-конус к f: X → Z и g: Y → Z. При ht — IsLimit, для любых h: W → X, k: W → Y и w: h ≫ f = k ≫ g, соответствующий стрелок IsLimit.lift ht h k w удовлетворяет (IsLimit.lift ht h k w) ≫ snd t = k.

LaTeX

$$$\\mathrm{IsLimit.lift}\\, ht\\, h\\, k\\, w \\;\\circ\\; \\mathrm{snd}(t) = k$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_snd {t : PullbackCone f g} (ht : IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : h ≫ f = k ≫ g) :
    IsLimit.lift ht h k w ≫ snd t = k :=
  ht.fac _ _

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