α : Type u_1
E : Type ?u.8098806
F : Type ?u.8098809
G : Type ?u.8098812
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
inst✝ : Fact (1 ≤ p)
eq : (fun f => negPart f) = fun f => posPart (-f)
⊢ Continuous fun f => negPart f
α : Type u_1
E : Type ?u.8098806
F : Type ?u.8098809
G : Type ?u.8098812
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
inst✝ : Fact (1 ≤ p)
⊢ Continuous fun f => negPart f
have eq : (fun f : Lp ℝ p μ => negPart f) = fun f : Lp ℝ p μ => posPart (-f) := rfl
α : Type u_1
E : Type ?u.8098806
F : Type ?u.8098809
G : Type ?u.8098812
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
inst✝ : Fact (1 ≤ p)
eq : (fun f => negPart f) = fun f => posPart (-f)
⊢ Continuous fun f => posPart (-f)
α : Type u_1
E : Type ?u.8098806
F : Type ?u.8098809
G : Type ?u.8098812
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
inst✝ : Fact (1 ≤ p)
eq : (fun f => negPart f) = fun f => posPart (-f)
⊢ Continuous fun f => negPart f
rw [eq]
no goals
α : Type u_1
E : Type ?u.8098806
F : Type ?u.8098809
G : Type ?u.8098812
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
inst✝ : Fact (1 ≤ p)
eq : (fun f => negPart f) = fun f => posPart (-f)
⊢ Continuous fun f => posPart (-f)
exact continuous_posPart.comp continuous_neg