eventually_pos — Mathlib

English

There exists a natural number k such that for all n ≥ k, n > 0 (i.e., eventually positive).

Русский

Существует натуральное число k такое, что для всех n ≥ k выполняется n > 0 (соответственно, вектор становится положительным вплоть до конца).

LaTeX

$$$\\exists k \\in \\mathbb{N}, \\forall n \\ge k, 0 < n$$$

Lean4

theorem eventually_pos : ∀ᶠ (k : ℕ) in Filter.atTop, 0 < k :=
  Filter.eventually_of_mem (Filter.mem_atTop_sets.mpr ⟨1, fun _ hx ↦ hx⟩) (fun _ hx ↦ hx)

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