lift_π — Mathlib

English

The relation lift F c ≫ π_j = c.π.app j holds for any cone c and any j, expressing the defining property of the limit lift.

Русский

Отношение lift F c ≫ π_j = c.π.app j верно для любого конуса c и любого j, выражая определяющее свойство lift предела.

LaTeX

$$$\\mathrm{limit}.lift F c \\;\\circ\\; \\mathrm{limit}.π F j = c.π.app j$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_π {F : J ⥤ C} [HasLimit F] (c : Cone F) (j : J) : limit.lift F c ≫ limit.π F j = c.π.app j :=
  IsLimit.fac _ c j

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