liftIoc_continuous — Mathlib

English

If h expresses that f(a)=f(a+p), then liftIoc is continuous as per liftIco continuity via the Icc reduction.

Русский

Если выполняется h: f(a)=f(a+p), то liftIoc непрерывна согласно непрерывности liftIco через редукцию Icc.

LaTeX

$$$$ \\text{If } f(a)=f(a+p), \\; \\mathrm{liftIoc}(p,a,f) \\text{ is continuous.} $$$$

Lean4

theorem liftIoc_continuous [TopologicalSpace B] {f : 𝕜 → B} (hf : f a = f (a + p))
    (hc : ContinuousOn f <| Icc a (a + p)) : Continuous (liftIoc p a f) :=
  by
  rw [liftIoc_eq_lift_Icc hf]
  refine Continuous.comp ?_ (homeoIccQuot p a).continuous_toFun
  exact continuous_coinduced_dom.mpr (continuousOn_iff_continuous_restrict.mp hc)

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