α : Type u_1
E : Type ?u.16086
F : Type ?u.16089
F' : Type ?u.16092
G : Type ?u.16095
𝕜 : Type ?u.16098
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T T' : Set α → β
hT : FinMeasAdditive μ T
hT' : FinMeasAdditive μ T'
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : ↑↑μ s ≠ ⊤
hμt : ↑↑μ t ≠ ⊤
hst : s ∩ t = ∅
⊢ (T + T') (s ∪ t) = (T + T') s + (T + T') t
α : Type u_1
E : Type ?u.16086
F : Type ?u.16089
F' : Type ?u.16092
G : Type ?u.16095
𝕜 : Type ?u.16098
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T T' : Set α → β
hT : FinMeasAdditive μ T
hT' : FinMeasAdditive μ T'
⊢ FinMeasAdditive μ (T + T')
intro s t hs ht hμs hμt hst
α : Type u_1
E : Type ?u.16086
F : Type ?u.16089
F' : Type ?u.16092
G : Type ?u.16095
𝕜 : Type ?u.16098
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T T' : Set α → β
hT : FinMeasAdditive μ T
hT' : FinMeasAdditive μ T'
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : ↑↑μ s ≠ ⊤
hμt : ↑↑μ t ≠ ⊤
hst : s ∩ t = ∅
⊢ T s + T t + (T' s + T' t) = T s + T' s + (T t + T' t)
α : Type u_1
E : Type ?u.16086
F : Type ?u.16089
F' : Type ?u.16092
G : Type ?u.16095
𝕜 : Type ?u.16098
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T T' : Set α → β
hT : FinMeasAdditive μ T
hT' : FinMeasAdditive μ T'
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : ↑↑μ s ≠ ⊤
hμt : ↑↑μ t ≠ ⊤
hst : s ∩ t = ∅
⊢ (T + T') (s ∪ t) = (T + T') s + (T + T') t
simp only [hT s t hs ht hμs hμt hst, hT' s t hs ht hμs hμt hst, Pi.add_apply]
no goals
α : Type u_1
E : Type ?u.16086
F : Type ?u.16089
F' : Type ?u.16092
G : Type ?u.16095
𝕜 : Type ?u.16098
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : AddCommMonoid β
T T' : Set α → β
hT : FinMeasAdditive μ T
hT' : FinMeasAdditive μ T'
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : ↑↑μ s ≠ ⊤
hμt : ↑↑μ t ≠ ⊤
hst : s ∩ t = ∅
⊢ T s + T t + (T' s + T' t) = T s + T' s + (T t + T' t)
abel