lift_π_apply — Mathlib

English

The j-th projection of limit.lift F s x equals the j-th component of the cone s evaluated at x.

Русский

Проекция j-го компонента limit.lift F s x равна j-й компоненте конуса s применительно к x.

LaTeX

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

Lean4

@[simp]
theorem lift_π_apply (s : Cone F) (j : J) (x : s.pt) : limit.π F j (limit.lift F s x) = s.π.app j x :=
  congr_fun (limit.lift_π s j) x

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