integrableOn_finite_biUnion — Mathlib

English

If the codomain is a singleton, every function is integrable on any set.

Русский

Если кодомодуль — одноэлементное множество, любая функция интегрируема на любом множестве.

LaTeX

$$$[Subsingleton\;\varepsilon'] \{f:\alpha\to\varepsilon'\} : \mathrm{IntegrableOn}(f,s,\mu)$$$

Lean4

@[simp]
theorem integrableOn_finite_biUnion [PseudoMetrizableSpace ε] {s : Set β} (hs : s.Finite) {t : β → Set α} :
    IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, IntegrableOn f (t i) μ := by
  induction s, hs using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ hf => simp [hf, or_imp, forall_and]

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