α : Type u_1
a : ℝ≥0∞
m : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ a * ↑m t = a * ↑m (t ∩ s) + a * ↑m (t \ s)
α : Type u_1
a : ℝ≥0∞
m : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ ↑(a • m) t = ↑(a • m) (t ∩ s) + ↑(a • m) (t \ s)
simp [smul_apply]
α : Type u_1
a : ℝ≥0∞
m : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ a * (↑m (t ∩ s) + ↑m (t \ s)) = a * ↑m (t ∩ s) + a * ↑m (t \ s)
α : Type u_1
a : ℝ≥0∞
m : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ a * ↑m t = a * ↑m (t ∩ s) + a * ↑m (t \ s)
rw [(isCaratheodory_iff m).mp h t]
no goals
α : Type u_1
a : ℝ≥0∞
m : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ a * (↑m (t ∩ s) + ↑m (t \ s)) = a * ↑m (t ∩ s) + a * ↑m (t \ s)
simp [mul_add]