coeFn_nonneg — Mathlib

English

Let f be an element of Lp(E, p, μ). Then f is nonnegative μ-almost everywhere if and only if its representative function is nonnegative at every point, i.e. 0 ≤ᵐμ f ⇔ 0 ≤ f.

Русский

Пусть f принадлежит пространству Lp(E, p, μ). Тогда f неотрицательно μ-асимптотически повсеместно тогда и только тогда, когда соответствующая функция-образец неотрицательна в каждой точке, т.е. 0 ≤ᵐμ f ⇔ 0 ≤ f.

LaTeX

$$$0 \le^{{\mathrm{ae}}}_\mu f \;\;\iff\;\; 0 \le f$$$

Lean4

theorem coeFn_nonneg (f : Lp E p μ) : 0 ≤ᵐ[μ] f ↔ 0 ≤ f :=
  by
  rw [← coeFn_le]
  have h0 := Lp.coeFn_zero E p μ
  constructor <;> intro h <;> filter_upwards [h, h0] with _ _ h2
  · rwa [h2]
  · rwa [← h2]

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