English
Let t: ℕ → β be strictly monotone with tendsto t atTop to atTop. For any x with t(0) < x, there exists n such that t(n) < x ≤ t(n+1).
Русский
Пусть t: ℕ → β строго возрастает и t(n) стремится к бесконечности. Тогда для любого x > t(0) существует n с t(n) < x ≤ t(n+1).
LaTeX
$$$ \text{Let } t: \mathbb{N} \to \beta \text{ strictly monotone and } \lim_{n\to\infty} t(n) = \infty.\ Then\ ∃ n:\ t(n) < x \le t(n+1).$$$
Lean4
theorem exists_between_of_tendsto_atTop {β : Type*} [LinearOrder β] {t : ℕ → β} (ht_mono : StrictMono t)
(ht_tendsto : Tendsto t atTop atTop) {x : β} (hx : t 0 < x) : ∃ n, t n < x ∧ x ≤ t (n + 1) :=
by
have h : ∃ n, x ≤ t n :=
by
simp only [tendsto_atTop_atTop_iff_of_monotone ht_mono.monotone] at ht_tendsto
exact ht_tendsto x
have h' m := Nat.find_min h (m := m)
simp only [not_le] at h' hx
exact ⟨Nat.find h - 1, h' _ (by simp [hx]), by simp [Nat.find_spec h, hx]⟩
