liftIoc_zero_coe_apply — Mathlib

English

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

Русский

Если x ∈ Ioc(0,p), то liftIoc(p,0,f) на каноническом представителе x равен f(x).

LaTeX

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

Lean4

theorem liftIoc_zero_coe_apply {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ Ioc 0 p) : liftIoc p 0 f ↑x = f x :=
  liftIoc_coe_apply (by rwa [zero_add])

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