integrableOn_uIoc — Mathlib

English

A continuous function with compact support is integrable over the whole space with respect to any locally finite measure on compacts.

Русский

Непрерывная функция с компактной опорой интегрируема на всей пространстве по любой локально конечной мере на компактах.

LaTeX

$$$\text{Continuous}(f) \land \operatorname{HasCompactSupport}(f) \Rightarrow \operatorname{Integrable}(f, \mu)$$$

Lean4

theorem integrableOn_uIoc [LinearOrder X] [CompactIccSpace X] [T2Space X] (hf : Continuous f) :
    IntegrableOn f (Ι a b) μ :=
  hf.integrableOn_Ioc

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