exists_eventually_const_mul_le_r — Mathlib

English

There exists c ∈ (0,1) such that for every n large enough, r_i(n) ≥ c n for all i.

Русский

Существует c ∈ (0,1), такой что для больших n выполняется r_i(n) ≥ c n для всех i.

LaTeX

$$$\exists c\in(0,1),\;\exists N\;\forall n\ge N,\; \forall i,\; r_i(n) \ge c\,n$$$

Lean4

theorem exists_eventually_const_mul_le_r : ∃ c ∈ Set.Ioo (0 : ℝ) 1, ∀ᶠ (n : ℕ) in atTop, ∀ i, c * n ≤ r i n :=
  by
  have gt_zero : 0 < b (min_bi b) := R.b_pos (min_bi b)
  exact ⟨b (min_bi b) / 2, ⟨⟨by positivity, R.bi_min_div_two_lt_one⟩, R.eventually_bi_mul_le_r⟩⟩

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