neg — Mathlib

English

Negation preserves Uniform Integrability: if f is UnifIntegrable, then −f is UnifIntegrable.

Русский

Непрерывное отрицательное преобразование сохраняет Uniform Integrability: если f — UnifIntegrable, то −f — тоже.

LaTeX

$$$\\operatorname{UnifIntegrable} f p μ \\Rightarrow \\operatorname{UnifIntegrable} (-f) p μ$$$

Lean4

protected theorem neg (hf : UnifIntegrable f p μ) : UnifIntegrable (-f) p μ :=
  by
  simp_rw [UnifIntegrable, Pi.neg_apply, Set.indicator_neg', eLpNorm_neg]
  exact hf

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