union — Mathlib

English

If f is IntegrableOn on s and on t with respect to μ, then it is IntegrableOn on s ∪ t with μ.

Русский

Если f интегрируема на s и на t по μ, то интегрируема на s ∪ t по μ.

LaTeX

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

Lean4

theorem union [PseudoMetrizableSpace ε] (hs : IntegrableOn f s μ) (ht : IntegrableOn f t μ) :
    IntegrableOn f (s ∪ t) μ :=
  (hs.add_measure ht).mono_measure <| Measure.restrict_union_le _ _

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