English
For an AEEqFun f taking values in a linearly ordered, order-closed topological space with zero, the positive part posPart(f) corresponds to the function x ↦ max(f(x), 0). This defines a new AEEqFun that encodes the positive part of f almost everywhere.
Русский
Для AEEqFun f, значения которого лежат в линейно упорядоченном пространстве с нулём, положительная часть posPart(f) соответствует функции x ↦ max(f(x), 0). Это даёт новую эквивалентную по почти всей мере AEEqFun, кодирующую положительную часть f.
LaTeX
$$$\operatorname{posPart}(f) \text{ соответствует функции } x \mapsto \max\{f(x), 0\}. $$$
Lean4
/-- Positive part of an `AEEqFun`. -/
def posPart (f : α →ₘ[μ] γ) : α →ₘ[μ] γ :=
comp (fun x => max x 0) (continuous_id.max continuous_const) f
