exists_bound — Mathlib

English

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

Русский

Если f абсолютно непрерывна на uIcc(a,b), то она ограничена на этом промежутке.

LaTeX

$$$\text{AbsolutelyContinuousOnInterval}(f,a,b) \Rightarrow \exists C\in \mathbb{R}, \; \forall x \in \mathrm{uIcc}(a,b), \; \|f(x)\| \le C$$$

Lean4

/-- If `f` is absolutely continuous on `uIcc a b`, then `f` is bounded on `uIcc a b`. -/
theorem exists_bound (hf : AbsolutelyContinuousOnInterval f a b) : ∃ (C : ℝ), ∀ x ∈ uIcc a b, ‖f x‖ ≤ C :=
  isCompact_Icc.exists_bound_of_continuousOn (hf.continuousOn)

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