lift_proj — Mathlib

English

Let c be a limit cone of a diagram X : β → C, and d be a cone on X with vertex A. Then hc.lift d followed by c.proj i equals d.proj i for every i ∈ β.

Русский

Пусть c — предел над диаграммой X : β → C, и d — любая верхняя система (конус) над X с вершиной A. Тогда hc.lift d ∘ c.proj_i = d.proj_i для всех i.

LaTeX

$$$\\forall i,\\; (hc.lift\,d) \\; \\circ \\; c.proj_i = d.proj_i$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_proj {X : β → C} {c : Fan X} (d : Fan X) (hc : IsLimit c) (i : β) : hc.lift d ≫ c.proj i = d.proj i :=
  hc.fac _ _

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