integrableOn_uIcc — Mathlib

English

If f is continuous on the uIcc of a and b, then f is integrable on that set with respect to μ.

Русский

Если f непрерывна на uIcc[a,b], то f интегрируема на этом множестве по μ.

LaTeX

$$$\operatorname{ContinuousOn}(f, \mathrm{uIcc}(a,b)) \Rightarrow \operatorname{IntegrableOn}(f, \mathrm{uIcc}(a,b), \mu)$$$

Lean4

theorem integrableOn_uIcc [LinearOrder X] [CompactIccSpace X] [T2Space X] (hf : ContinuousOn f [[a, b]]) :
    IntegrableOn f [[a, b]] μ :=
  hf.integrableOn_Icc

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