coeFn_negPart_eq_max — Mathlib

English

Let f be an Lp-function. Then almost everywhere, the negative part of f equals the maximum of -f and 0: negPart f = max(-f, 0) a.e.

Русский

Пусть f — функция из Lp. Тогда почти всюду выполняется равенство отрицательной части: negPart f = max(-f, 0) а.e.

LaTeX

$$$\forall f\; (\mu-a.e.\;\negPart f = \max(-f,0))$$$

Lean4

theorem coeFn_negPart_eq_max (f : Lp ℝ p μ) : ∀ᵐ a ∂μ, negPart f a = max (-f a) 0 :=
  by
  rw [negPart]
  filter_upwards [coeFn_posPart (-f), coeFn_neg f] with _ h₁ h₂
  rw [h₁, h₂, Pi.neg_apply]

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