English
For a lattice-ordered codomain β with appropriate topological structure, the absolute value of f coerces almost everywhere to the absolute value of f(x).
Русский
Для β с линейной структурой и подходящей топологической структурой модульной функции, модуля f переходит к almost everywhere к |f(x)|.
LaTeX
$$coeFn_abs {β} [TopologicalSpace β] [Lattice β] [TopologicalLattice β] [AddGroup β] [IsTopologicalAddGroup β] (f : α →ₘ[μ] β) : ↑|f| =ᵐ[μ] fun x => |f x|$$
Lean4
theorem coeFn_abs {β} [TopologicalSpace β] [Lattice β] [TopologicalLattice β] [AddGroup β] [IsTopologicalAddGroup β]
(f : α →ₘ[μ] β) : ⇑|f| =ᵐ[μ] fun x => |f x| := by
simp_rw [abs]
filter_upwards [AEEqFun.coeFn_sup f (-f), AEEqFun.coeFn_neg f] with x hx_sup hx_neg
rw [hx_sup, hx_neg, Pi.neg_apply]
