integrableOn_union — Mathlib

English

For f integrable on s ∪ t with μ, f is integrable on s and on t; conversely, integrability on s and on t implies integrability on s ∪ t.

Русский

Для интегрируемости f на s ∪ t по μ эквивалентно интегрируемости на s и на t по μ, и обратно.

LaTeX

$$$\mathrm{IntegrableOn}(f,s\cup t,\mu) \iff \mathrm{IntegrableOn}(f,s,\mu) \land \mathrm{IntegrableOn}(f,t,\mu)$$$

Lean4

@[simp]
theorem integrableOn_union [PseudoMetrizableSpace ε] :
    IntegrableOn f (s ∪ t) μ ↔ IntegrableOn f s μ ∧ IntegrableOn f t μ :=
  ⟨fun h => ⟨h.left_of_union, h.right_of_union⟩, fun h => h.1.union h.2⟩

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