weightedSMul_union' — Mathlib

English

For disjoint sets s and t with measurability and finite measures, the weightedSMul over their union equals the sum of the weightedSMuls: weightedSMul μ (s ∪ t) = weightedSMul μ s + weightedSMul μ t.

Русский

Для непересекающихся множеств s и t при измеримости и конечности мер: weightedSMul μ (s ∪ t) = weightedSMul μ s + weightedSMul μ t.

LaTeX

$$$$weightedSMul\,\mu( s \cup t) = weightedSMul\,\mu s + weightedSMul\,\mu t.$$$$

Lean4

theorem weightedSMul_union' (s t : Set α) (ht : MeasurableSet t) (hs_finite : μ s ≠ ∞) (ht_finite : μ t ≠ ∞)
    (hdisj : Disjoint s t) : (weightedSMul μ (s ∪ t) : F →L[ℝ] F) = weightedSMul μ s + weightedSMul μ t :=
  by
  ext1 x
  simp_rw [add_apply, weightedSMul_apply, measureReal_union hdisj ht, add_smul]

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