continuousOn — Mathlib

English

If f is absolutely continuous on uIcc(a,b), then f is continuous on uIcc(a,b).

Русский

Если f абсолютно непрерывна на uIcc(a,b), то она непрерывна на uIcc(a,b).

LaTeX

$$$\text{AbsolutelyContinuousOnInterval}(f,a,b) \Rightarrow \text{ContinuousOn}(f, \mathrm{uIcc}(a,b))$$$

Lean4

/-- If `f` is absolutely continuous on `uIcc a b`, then `f` is continuous on `uIcc a b`. -/
theorem continuousOn (hf : AbsolutelyContinuousOnInterval f a b) : ContinuousOn f (uIcc a b) :=
  hf.uniformlyContinuousOn.continuousOn

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