liftIco_continuous — Mathlib

English

If f is continuous on the interval Icc(a,a+p) and f(a)=f(a+p), then the lifted map liftIco(p,a,f) is continuous on the interval Icc(a,a+p).

Русский

Если f непрерывна на отрезке Icc(a,a+p) и f(a)=f(a+p), то подъем liftIco(p,a,f) непрерывен на Icc(a,a+p).

LaTeX

$$$$ \\text{If } f(a)=f(a+p) \\text{ and } f \\text{ is continuous on } Icc(a,a+p), \\; \\mathrm{liftIco}(p,a,f) \\text{ is continuous.} $$$$

Lean4

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

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