map_π_apply' — Mathlib

English

A restatement of map_π_apply with explicit domain/codomain; the same equality holds.

Русский

Переформулирование map_π_apply с явным выводом: выполняется то же равенство.

LaTeX

$$$\forall {F G : J ⥤ Type u}\ [HasLimit F] [HasLimit G] (\alpha : F ⟶ G) (j : J) (x : limit F),\; limit.\pi G j (limMap \alpha x) = \alpha.\app j (limit.\pi F j x).$$$

Lean4

theorem map_π_apply' {F G : J ⥤ Type v} (α : F ⟶ G) (j : J) (x : limit F) :
    limit.π G j (limMap α x) = α.app j (limit.π F j x) :=
  congr_fun (limMap_π α j) x

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