α : Type u_2
β✝ : Type ?u.1579337
γ : Type ?u.1579340
δ : Type ?u.1579343
inst✝⁸ : MeasurableSpace α
μ ν : Measure α
inst✝⁷ : TopologicalSpace β✝
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : TopologicalSpace δ
β : Type u_1
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
f : α →ₘ[μ] β
⊢ ↑(f ⊔ -f) =ᵐ[μ] fun x => ↑f x ⊔ -↑f x
α : Type u_2
β✝ : Type ?u.1579337
γ : Type ?u.1579340
δ : Type ?u.1579343
inst✝⁸ : MeasurableSpace α
μ ν : Measure α
inst✝⁷ : TopologicalSpace β✝
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : TopologicalSpace δ
β : Type u_1
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
f : α →ₘ[μ] β
⊢ ↑(abs f) =ᵐ[μ] fun x => abs (↑f x)
simp_rw [abs_eq_sup_neg]
case h
α : Type u_2
β✝ : Type ?u.1579337
γ : Type ?u.1579340
δ : Type ?u.1579343
inst✝⁸ : MeasurableSpace α
μ ν : Measure α
inst✝⁷ : TopologicalSpace β✝
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : TopologicalSpace δ
β : Type u_1
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
f : α →ₘ[μ] β
x : α
hx_sup : ↑(f ⊔ -f) x = ↑f x ⊔ ↑(-f) x
hx_neg : ↑(-f) x = (-↑f) x
⊢ ↑(f ⊔ -f) x = ↑f x ⊔ -↑f x
α : Type u_2
β✝ : Type ?u.1579337
γ : Type ?u.1579340
δ : Type ?u.1579343
inst✝⁸ : MeasurableSpace α
μ ν : Measure α
inst✝⁷ : TopologicalSpace β✝
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : TopologicalSpace δ
β : Type u_1
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
f : α →ₘ[μ] β
⊢ ↑(f ⊔ -f) =ᵐ[μ] fun x => ↑f x ⊔ -↑f x
filter_upwards [AEEqFun.coeFn_sup f (-f), AEEqFun.coeFn_neg f] with x hx_sup hx_neg
no goals
case h
α : Type u_2
β✝ : Type ?u.1579337
γ : Type ?u.1579340
δ : Type ?u.1579343
inst✝⁸ : MeasurableSpace α
μ ν : Measure α
inst✝⁷ : TopologicalSpace β✝
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : TopologicalSpace δ
β : Type u_1
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
f : α →ₘ[μ] β
x : α
hx_sup : ↑(f ⊔ -f) x = ↑f x ⊔ ↑(-f) x
hx_neg : ↑(-f) x = (-↑f) x
⊢ ↑(f ⊔ -f) x = ↑f x ⊔ -↑f x
rw [hx_sup, hx_neg, Pi.neg_apply]