liftIco_zero_coe_apply — Mathlib

English

If x lies in Ico(0,p), then liftIco(p,0,f) evaluated at the canonical representative x equals f(x).

Русский

Если x лежит в Ico(0,p), то liftIco(p,0,f) на каноническом представителе x даёт f(x).

LaTeX

$$$$ \\forall x \\in \\mathrm{Ico}(0,p), \\; \\mathrm{liftIco}(p,0,f,\\mathrm{QuotientAddGroup.mk} x) = f(x). $$$$

Lean4

theorem liftIco_zero_coe_apply {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ Ico 0 p) : liftIco p 0 f ↑x = f x :=
  liftIco_coe_apply (by rwa [zero_add])

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