neg — Mathlib

English

If f grows polynomially, then its negation −f also grows polynomially (and vice versa).

Русский

Если f растёт полиномиально, то и −f растёт полиномиально (и наоборот).

LaTeX

$$$\\text{GrowsPolynomially}(f) \\Rightarrow \\text{GrowsPolynomially}(-f)\\quad\\text{and}\\quad \\text{GrowsPolynomially}(-f) \\Rightarrow \\text{GrowsPolynomially}(f)$$$

Lean4

protected theorem neg {f : ℝ → ℝ} (hf : GrowsPolynomially f) : GrowsPolynomially (-f) :=
  by
  intro b hb
  obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf b hb
  refine ⟨c₂, hc₂_mem, c₁, hc₁_mem, ?_⟩
  filter_upwards [hf] with x hx
  intro u hu
  simp only [Pi.neg_apply, Set.neg_mem_Icc_iff, neg_mul_eq_mul_neg, neg_neg]
  exact hx u hu

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