coeFn_posPart — Mathlib

English

The a.e. representative of posPart(f) is the almost-everywhere pointwise maximum with zero: the underlying function is max(f(a), 0) almost everywhere.

Русский

Представляющая почти везде часть posPart(f) совпадает с функцией max(f(a), 0) почти повсеместно.

LaTeX

$$$\iota_{\text{posPart}}(f) \;=\; \max\bigl(f, 0\bigr) \quad \text{a.e.} $$$

Lean4

theorem coeFn_posPart (f : α →ₘ[μ] γ) : ⇑(posPart f) =ᵐ[μ] fun a => max (f a) 0 :=
  coeFn_comp _ _ _

Похожие утверждения