α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.671027
G : Type ?u.671030
𝕜 : Type ?u.671033
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✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f : { x // x ∈ simpleFunc E 1 μ }
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (-f)) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.671027
G : Type ?u.671030
𝕜 : Type ?u.671033
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✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f : { x // x ∈ simpleFunc E 1 μ }
⊢ setToL1S T (-f) = -setToL1S T f
simp_rw [setToL1S]
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.671027
G : Type ?u.671030
𝕜 : Type ?u.671033
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✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f : { x // x ∈ simpleFunc E 1 μ }
this : ↑(toSimpleFunc (-f)) =ᵐ[μ] ↑(-toSimpleFunc f)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (-f)) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.671027
G : Type ?u.671030
𝕜 : Type ?u.671033
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✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f : { x // x ∈ simpleFunc E 1 μ }
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (-f)) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
have : simpleFunc.toSimpleFunc (-f) =ᵐ[μ] ⇑(-simpleFunc.toSimpleFunc f) :=
  neg_toSimpleFunc f
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.671027
G : Type ?u.671030
𝕜 : Type ?u.671033
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✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f : { x // x ∈ simpleFunc E 1 μ }
this : ↑(toSimpleFunc (-f)) =ᵐ[μ] ↑(-toSimpleFunc f)
⊢ SimpleFunc.setToSimpleFunc T (-toSimpleFunc f) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.671027
G : Type ?u.671030
𝕜 : Type ?u.671033
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✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f : { x // x ∈ simpleFunc E 1 μ }
this : ↑(toSimpleFunc (-f)) =ᵐ[μ] ↑(-toSimpleFunc f)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (-f)) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
rw [SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _) this]
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.671027
G : Type ?u.671030
𝕜 : Type ?u.671033
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✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f : { x // x ∈ simpleFunc E 1 μ }
this : ↑(toSimpleFunc (-f)) =ᵐ[μ] ↑(-toSimpleFunc f)
⊢ SimpleFunc.setToSimpleFunc T (-toSimpleFunc f) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
exact SimpleFunc.setToSimpleFunc_neg T h_add (SimpleFunc.integrable f)