term_nonneg — Mathlib

English

If a_n ≥ 0, then term a x n ≥ 0 for all x ∈ ℝ, i.e., nonnegativity is preserved.

Русский

Если a_n ≥ 0, то term a x n ≥ 0 для всех x ∈ ℝ; неотрицательность сохраняется.

LaTeX

$$$a_ n \\ge 0 \\Rightarrow \\operatorname{term}(a,x,n) \\ge 0$ for all x ∈ ℝ$$

Lean4

theorem term_nonneg {a : ℕ → ℂ} {n : ℕ} (h : 0 ≤ a n) (x : ℝ) : 0 ≤ term a x n :=
  by
  rw [term_def]
  split_ifs with hn
  exacts [le_rfl, mul_nonneg h (inv_natCast_cpow_ofReal_pos hn x).le]

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