map_π_apply — Mathlib

English

A restatement of limit.lift projection behavior using explicit symbols.

Русский

Переформулировка поведения проекции limit.lift с явными обозначениями.

LaTeX

$$$\mathrm{limit.\pi} F j (\mathrm{limit.lift} F s x) = s.\pi.app j x.$$$

Lean4

@[simp]
theorem map_π_apply {F G : J ⥤ Type u} [HasLimit F] [HasLimit G] (α : F ⟶ G) (j : J) (x : limit F) :
    limit.π G j (limMap α x) = α.app j (limit.π F j x) :=
  congr_fun (limMap_π α j) x

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