α : Type u_2
E : Type ?u.33868
F : Type ?u.33871
F' : Type ?u.33874
G : Type ?u.33877
𝕜 : Type ?u.33880
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.34180
inst✝¹ : AddCommMonoid β✝
T✝ T' : Set α → β✝
β : Type u_1
inst✝ : AddCancelMonoid β
T : Set α → β
hT : FinMeasAdditive μ T
h_empty : ↑↑μ ∅ ≠ ⊤
⊢ T ∅ = 0
α : Type u_2
E : Type ?u.33868
F : Type ?u.33871
F' : Type ?u.33874
G : Type ?u.33877
𝕜 : Type ?u.33880
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.34180
inst✝¹ : AddCommMonoid β✝
T✝ T' : Set α → β✝
β : Type u_1
inst✝ : AddCancelMonoid β
T : Set α → β
hT : FinMeasAdditive μ T
⊢ T ∅ = 0
have h_empty : μ ∅ ≠ ∞ := (measure_empty.le.trans_lt ENNReal.coe_lt_top).ne
α : Type u_2
E : Type ?u.33868
F : Type ?u.33871
F' : Type ?u.33874
G : Type ?u.33877
𝕜 : Type ?u.33880
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.34180
inst✝¹ : AddCommMonoid β✝
T✝ T' : Set α → β✝
β : Type u_1
inst✝ : AddCancelMonoid β
T : Set α → β
h_empty : ↑↑μ ∅ ≠ ⊤
hT : T (∅ ∪ ∅) = T ∅ + T ∅
⊢ T ∅ = 0
α : Type u_2
E : Type ?u.33868
F : Type ?u.33871
F' : Type ?u.33874
G : Type ?u.33877
𝕜 : Type ?u.33880
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.34180
inst✝¹ : AddCommMonoid β✝
T✝ T' : Set α → β✝
β : Type u_1
inst✝ : AddCancelMonoid β
T : Set α → β
hT : FinMeasAdditive μ T
h_empty : ↑↑μ ∅ ≠ ⊤
⊢ T ∅ = 0
specialize hT ∅ ∅ MeasurableSet.empty MeasurableSet.empty h_empty h_empty (Set.inter_empty ∅)
α : Type u_2
E : Type ?u.33868
F : Type ?u.33871
F' : Type ?u.33874
G : Type ?u.33877
𝕜 : Type ?u.33880
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.34180
inst✝¹ : AddCommMonoid β✝
T✝ T' : Set α → β✝
β : Type u_1
inst✝ : AddCancelMonoid β
T : Set α → β
h_empty : ↑↑μ ∅ ≠ ⊤
hT : T ∅ = T ∅ + T ∅
⊢ T ∅ = 0
α : Type u_2
E : Type ?u.33868
F : Type ?u.33871
F' : Type ?u.33874
G : Type ?u.33877
𝕜 : Type ?u.33880
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.34180
inst✝¹ : AddCommMonoid β✝
T✝ T' : Set α → β✝
β : Type u_1
inst✝ : AddCancelMonoid β
T : Set α → β
h_empty : ↑↑μ ∅ ≠ ⊤
hT : T (∅ ∪ ∅) = T ∅ + T ∅
⊢ T ∅ = 0
rw [Set.union_empty] at hT
α : Type u_2
E : Type ?u.33868
F : Type ?u.33871
F' : Type ?u.33874
G : Type ?u.33877
𝕜 : Type ?u.33880
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.34180
inst✝¹ : AddCommMonoid β✝
T✝ T' : Set α → β✝
β : Type u_1
inst✝ : AddCancelMonoid β
T : Set α → β
h_empty : ↑↑μ ∅ ≠ ⊤
hT : T ∅ + 0 = T ∅ + T ∅
⊢ T ∅ = 0
α : Type u_2
E : Type ?u.33868
F : Type ?u.33871
F' : Type ?u.33874
G : Type ?u.33877
𝕜 : Type ?u.33880
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.34180
inst✝¹ : AddCommMonoid β✝
T✝ T' : Set α → β✝
β : Type u_1
inst✝ : AddCancelMonoid β
T : Set α → β
h_empty : ↑↑μ ∅ ≠ ⊤
hT : T ∅ = T ∅ + T ∅
⊢ T ∅ = 0
nth_rw 1 [← add_zero (T ∅)] at hT
no goals
α : Type u_2
E : Type ?u.33868
F : Type ?u.33871
F' : Type ?u.33874
G : Type ?u.33877
𝕜 : Type ?u.33880
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.34180
inst✝¹ : AddCommMonoid β✝
T✝ T' : Set α → β✝
β : Type u_1
inst✝ : AddCancelMonoid β
T : Set α → β
h_empty : ↑↑μ ∅ ≠ ⊤
hT : T ∅ + 0 = T ∅ + T ∅
⊢ T ∅ = 0
exact (add_left_cancel hT).symm