integrableOn_Ioc — 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_Ioc [Preorder X] [CompactIccSpace X] [T2Space X] (hf : Continuous f) :
    IntegrableOn f (Ioc a b) μ :=
  hf.integrableOn_Icc.mono_set Ioc_subset_Icc_self

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