case H
α : Type u_1
E : Type ?u.92838
F : Type ?u.92841
𝕜 : Type ?u.92844
inst✝² : LinearOrder E
inst✝¹ : Zero E
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a✝ : α
⊢ ↑(map norm (posPart f)) a✝ = ↑(posPart f) a✝
α : Type u_1
E : Type ?u.92838
F : Type ?u.92841
𝕜 : Type ?u.92844
inst✝² : LinearOrder E
inst✝¹ : Zero E
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ map norm (posPart f) = posPart f
ext
case H
α : Type u_1
E : Type ?u.92838
F : Type ?u.92841
𝕜 : Type ?u.92844
inst✝² : LinearOrder E
inst✝¹ : Zero E
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a✝ : α
⊢ 0 ≤ ↑(posPart f) a✝
case H
α : Type u_1
E : Type ?u.92838
F : Type ?u.92841
𝕜 : Type ?u.92844
inst✝² : LinearOrder E
inst✝¹ : Zero E
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a✝ : α
⊢ ↑(map norm (posPart f)) a✝ = ↑(posPart f) a✝
rw [map_apply, Real.norm_eq_abs, abs_of_nonneg]
no goals
case H
α : Type u_1
E : Type ?u.92838
F : Type ?u.92841
𝕜 : Type ?u.92844
inst✝² : LinearOrder E
inst✝¹ : Zero E
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a✝ : α
⊢ 0 ≤ ↑(posPart f) a✝
exact le_max_right _ _