integrableOn_compact — Mathlib

English

A similar decomposition exists for integrability on Iio with nhdsWithin, relating bottom, nhdsWithin, and local integrability on Iio.

Русский

Для Iio с nhdsWithin существует аналогичное разложение, связывающее atBot, nhdsWithin и локальную интегрируемость на Iio.

LaTeX

$$$\operatorname{IntegrableOn}(f, \mathrm{Iio}(a), \mu) \iff \bigl( \operatorname{IntegrableAtFilter}(f, \text{atBot}, \mu) \land \operatorname{IntegrableAtFilter}(f, \mathcal{nhdsWithin}(a, \mathrm{Iio}(a)), \mu) \land \operatorname{LocallyIntegrableOn}(f, \mathrm{Iio}(a), \mu) \bigr)$$$

Lean4

theorem integrableOn_compact [T2Space X] (hK : IsCompact K) (hf : ContinuousOn f K) : IntegrableOn f K μ :=
  hf.integrableOn_compact' hK hK.measurableSet

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