coeFn_nonneg — Mathlib

English

A nonnegative simple function corresponds a.e. to a nonnegative function.

Русский

Неотрицательная простая функция эквивалентна неотрицательной функции almost everywhere.

LaTeX

$$$\text{coeFn_nonneg}\; (f) : (0 ≤ f) \;\Leftrightarrow\; (0 ≤ f)$$$

Lean4

theorem coeFn_nonneg (f : Lp.simpleFunc G p μ) : (0 : α → G) ≤ᵐ[μ] f ↔ 0 ≤ f := by
  rw [← Subtype.coe_le_coe, Lp.coeFn_nonneg, AddSubmonoid.coe_zero]

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