α : Type u_1
E : Type ?u.93564
F : Type ?u.93567
𝕜 : Type ?u.93570
inst✝² : LinearOrder E
inst✝¹ : Zero E
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ map norm (posPart (-f)) = posPart (-f)
α : Type u_1
E : Type ?u.93564
F : Type ?u.93567
𝕜 : Type ?u.93570
inst✝² : LinearOrder E
inst✝¹ : Zero E
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ map norm (negPart f) = negPart f
rw [negPart]
no goals
α : Type u_1
E : Type ?u.93564
F : Type ?u.93567
𝕜 : Type ?u.93570
inst✝² : LinearOrder E
inst✝¹ : Zero E
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ map norm (posPart (-f)) = posPart (-f)
exact posPart_map_norm _