integrableOn_finset_iUnion — Mathlib

English

If μ is finite and f is AEStronglyMeasurable and essentially bounded by C, then f is integrable.

Русский

Если μ конечна и f измерима и по существу ограничена константой C, то f интегрируема.

LaTeX

$$$[IsFiniteMeasure\;\mu] \Rightarrow \mathrm{AEStronglyMeasurable}(f,\mu) \to (\forall C \in \mathbb{R}, \forall^{\ast} x\partial\mu, \|f(x)\| \le C) \to \mathrm{Integrable}(f,\mu)$$$

Lean4

@[simp]
theorem integrableOn_finset_iUnion [PseudoMetrizableSpace ε] {s : Finset β} {t : β → Set α} :
    IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, IntegrableOn f (t i) μ :=
  integrableOn_finite_biUnion s.finite_toSet

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