neg — Mathlib

English

If f is uniformly tight with respect to p and μ, then the function −f is also uniformly tight with respect to p and μ.

Русский

Если функция f обладает униформной ограниченностью (tightness) по отношению к p и μ, то и функция −f обладает той же собственно по отношению к p и μ.

LaTeX

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

Lean4

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

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