liftIoc_zero_continuous — Mathlib

English

If the endpoint condition holds, liftIoc coincides with liftIco for all x, preserving continuity.

Русский

При условии на концах поднятие liftIoc совпадает с liftIco для всех x и сохраняет непрерывность.

LaTeX

$$$$ \\mathrm{liftIoc}(p,0,f) = \\mathrm{liftIco}(p,0,f) $$ в случае допустимости условия на границе, и сохраняет непрерывность. $$$$

Lean4

theorem liftIoc_zero_continuous [TopologicalSpace B] {f : 𝕜 → B} (hf : f 0 = f p) (hc : ContinuousOn f <| Icc 0 p) :
    Continuous (liftIoc p 0 f) :=
  liftIoc_continuous (by rwa [zero_add] : f 0 = f (0 + p)) (by rwa [zero_add])

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