integrableOn_Icc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem integrableOn_Icc [Preorder X] [CompactIccSpace X] [T2Space X] (hf : Continuous f) :
    IntegrableOn f (Icc a b) μ :=
  hf.continuousOn.integrableOn_Icc

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