neg_iff — Mathlib

English

A function grows polynomially if and only if its negation grows polynomially.

Русский

Функция растёт полиномиально тогда и только тогда, когда её отрицание растёт полиномиально.

LaTeX

$$$\\text{GrowsPolynomially}(f) \\Leftrightarrow \\text{GrowsPolynomially}(-f)$$$

Lean4

protected theorem neg_iff {f : ℝ → ℝ} : GrowsPolynomially f ↔ GrowsPolynomially (-f) :=
  ⟨fun hf => hf.neg, fun hf => by rw [← neg_neg f]; exact hf.neg⟩

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