case pos
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1458556
G : Type ?u.1458559
𝕜 : Type ?u.1458562
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 α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : Integrable f
⊢ setToFun μ T hT (-f) = -setToFun μ T hT f

case neg
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1458556
G : Type ?u.1458559
𝕜 : Type ?u.1458562
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 α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : ¬Integrable f
⊢ setToFun μ T hT (-f) = -setToFun μ T hT f
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1458556
G : Type ?u.1458559
𝕜 : Type ?u.1458562
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 α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive μ T C
f : α → E
⊢ setToFun μ T hT (-f) = -setToFun μ T hT f
by_cases hf : Integrable f μ
no goals
case pos
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1458556
G : Type ?u.1458559
𝕜 : Type ?u.1458562
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 α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : Integrable f
⊢ setToFun μ T hT (-f) = -setToFun μ T hT f
rw [setToFun_eq hT hf, setToFun_eq hT hf.neg, Integrable.toL1_neg,
  (L1.setToL1 hT).map_neg]
case neg
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1458556
G : Type ?u.1458559
𝕜 : Type ?u.1458562
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 α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : ¬Integrable f
⊢ ¬Integrable (-f)
case neg
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1458556
G : Type ?u.1458559
𝕜 : Type ?u.1458562
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 α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : ¬Integrable f
⊢ setToFun μ T hT (-f) = -setToFun μ T hT f
rw [setToFun_undef hT hf, setToFun_undef hT, neg_zero]
no goals
case neg
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1458556
G : Type ?u.1458559
𝕜 : Type ?u.1458562
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 α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : ¬Integrable f
⊢ ¬Integrable (-f)
rwa [← integrable_neg_iff] at hf