weightedSMul_add_measure — Mathlib

English

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

Русский

Для разнесённых по набору s и t взвешенная по их объединению равна сумме взвешенных по каждому из них.

LaTeX

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

Lean4

theorem weightedSMul_add_measure {m : MeasurableSpace α} (μ ν : Measure α) {s : Set α} (hμs : μ s ≠ ∞) (hνs : ν s ≠ ∞) :
    (weightedSMul (μ + ν) s : F →L[ℝ] F) = weightedSMul μ s + weightedSMul ν s :=
  by
  ext1 x
  push_cast
  simp_rw [Pi.add_apply, weightedSMul_apply]
  rw [measureReal_add_apply, add_smul]

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