nonneg_of_eventually_pow_nonneg — Mathlib

English

In a ring with a strict order, if a^n ≥ 0 eventually for all large n, then a ≥ 0.

Русский

В кольце с жёстким упорядочением, если a^n becomes nonnegative eventually, то a ≥ 0.

LaTeX

$$$\\forall \\alpha [\\text{Ring } \\alpha] [\\text{LinearOrder } \\alpha] [\\text{IsStrictOrderedRing } \\alpha],\\; (\\forall^{\\infty} n \\in \\operatorname{atTop}, 0 \\le a^{n}) \\Rightarrow 0 \\le a$$$

Lean4

theorem nonneg_of_eventually_pow_nonneg {α : Type*} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a : α}
    (h : ∀ᶠ n in atTop, 0 ≤ a ^ (n : ℕ)) : 0 ≤ a :=
  let ⟨_n, ho, hn⟩ := (Nat.frequently_odd.and_eventually h).exists
  ho.pow_nonneg_iff.1 hn

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