English
If x ≤ liminf u atTop and the sequence is bounded, then there exists n with x + ε > u n.
Русский
Если x ≤ liminf u atTop и последовательность ограничена, существует n, такое что x + ε > u(n).
LaTeX
$$∃ n : PNat, x + ε < u n$$
Lean4
/-- If `Filter.limsup u atTop ≤ x`, then for all `ε > 0`, there exists a positive natural
number `n` such that `u n < x + ε`. -/
theorem exists_lt_of_limsup_le [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : ℕ → α}
(hu_bdd : IsBoundedUnder LE.le atTop u) (hu : Filter.limsup u atTop ≤ x) (hε : 0 < ε) : ∃ n : PNat, u n < x + ε :=
by
have h : ∀ᶠ n : ℕ in atTop, u n < x + ε := eventually_lt_add_pos_of_limsup_le hu_bdd hu hε
simp only [eventually_atTop] at h
obtain ⟨n, hn⟩ := h
exact ⟨⟨n + 1, Nat.succ_pos _⟩, hn (n + 1) (Nat.le_succ _)⟩
