w — Mathlib · SciLib

English

The inv component of the cone point unique up to iso interacts with π to recover the cone's legs, i.e., (IsLimit.conePointUniqueUpToIso).inv ≫ limit.π F j = c.π.app j.

Русский

Обратная часть изоморфизма конусной точки совместима с π: inv ≫ π_j = c.π.app j.

LaTeX

$$$(\\mathrm{IsLimit}.conePointUniqueUpToIso (\\mathrm{limit}.isLimit F)).inv \\;\\circ\\; \\mathrm{limit}.π F j = c.π.app j$$$

Lean4

@[reassoc (attr := simp)]
theorem w (F : J ⥤ C) [HasLimit F] {j j' : J} (f : j ⟶ j') : limit.π F j ≫ F.map f = limit.π F j' :=
  (limit.cone F).w f

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