English
For a directed preordered set, if limsup ≤ x, then there exists a such that p a’s hold in eventual sense.
Русский
Для направленного частично упорядоченного множества, если limsup ≤ x, существует элемент a, удовлетворяющий p в пределе.
LaTeX
$$Exists a, ∀ b with b ≥ a, p b$$
Lean4
/-- If `x ≤ Filter.liminf u atTop`, then for all `ε < 0`, there exists a positive natural
number `n` such that ` x + ε < u n`. -/
theorem exists_lt_of_le_liminf [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : ℕ → α}
(hu_bdd : IsBoundedUnder GE.ge atTop u) (hu : x ≤ Filter.liminf u atTop) (hε : ε < 0) : ∃ n : PNat, x + ε < u n :=
by
have h : ∀ᶠ n : ℕ in atTop, x + ε < u n := eventually_add_neg_lt_of_le_liminf 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 _)⟩
