max_zero — Mathlib

English

For a unit c in a NormedRing 𝕜, HasFiniteIntegral (c • f) μ ⇔ HasFiniteIntegral f μ.

Русский

Для единицы c в нормированном кольце 𝕜 имеем эквивалентность HasFiniteIntegral (c • f) μ и HasFiniteIntegral f μ.

LaTeX

$$$\text{IsUnit } c \Rightarrow (HasFiniteIntegral (c \cdot f) μ \iff HasFiniteIntegral f μ)$$$

Lean4

@[fun_prop]
theorem max_zero {f : α → ℝ} (hf : HasFiniteIntegral f μ) : HasFiniteIntegral (fun a => max (f a) 0) μ :=
  hf.mono <| Eventually.of_forall fun x => by simp [abs_le, le_abs_self]

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