integrable_of_hasCompactSupport — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- A continuous function with compact support is integrable on the whole space. -/
theorem integrable_of_hasCompactSupport (hf : Continuous f) (hcf : HasCompactSupport f) : Integrable f μ :=
  (integrableOn_iff_integrable_of_support_subset (subset_tsupport f)).mp <|
    hf.continuousOn.integrableOn_compact' hcf (isClosed_tsupport _).measurableSet

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