integrableOn_finite_iUnion — Mathlib

English

If h is IntegrableOn f s μ, then h is IntegrableOn f s (μ.restrict t).

Русский

Если h интегрируемо на f на s по μ, то интегрируемо на f на s по μ|_t.

LaTeX

$$$\mathrm{IntegrableOn}(f,s,\mu) \to \mathrm{IntegrableOn}(f,s,\mu|_{t})$$$

Lean4

@[simp]
theorem integrableOn_finite_iUnion [PseudoMetrizableSpace ε] [Finite β] {t : β → Set α} :
    IntegrableOn f (⋃ i, t i) μ ↔ ∀ i, IntegrableOn f (t i) μ :=
  by
  cases nonempty_fintype β
  simpa using
    integrableOn_finset_iUnion (f := f) (μ := μ) (s := Finset.univ) (t := t)
      -- TODO: generalise this lemma and the next to enorm classes; this entails assuming that
      -- f is finite on almost every element of `s`

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