case h
α : Type u_1
E : Type ?u.49399
F : Type u_2
𝕜 : Type ?u.49405
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
hs_finite : ↑↑μ s ≠ ⊤
ht_finite : ↑↑μ t ≠ ⊤
h_inter : s ∩ t = ∅
x : F
⊢ ↑(weightedSMul μ (s ∪ t)) x = ↑(weightedSMul μ s + weightedSMul μ t) x
α : Type u_1
E : Type ?u.49399
F : Type u_2
𝕜 : Type ?u.49405
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
hs_finite : ↑↑μ s ≠ ⊤
ht_finite : ↑↑μ t ≠ ⊤
h_inter : s ∩ t = ∅
⊢ weightedSMul μ (s ∪ t) = weightedSMul μ s + weightedSMul μ t
ext1 x
no goals
case h
α : Type u_1
E : Type ?u.49399
F : Type u_2
𝕜 : Type ?u.49405
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
hs_finite : ↑↑μ s ≠ ⊤
ht_finite : ↑↑μ t ≠ ⊤
h_inter : s ∩ t = ∅
x : F
⊢ ↑(weightedSMul μ (s ∪ t)) x = ↑(weightedSMul μ s + weightedSMul μ t) x
simp_rw [add_apply, weightedSMul_apply,
  measure_union (Set.disjoint_iff_inter_eq_empty.mpr h_inter) ht,
  ENNReal.toReal_add hs_finite ht_finite, add_smul]