English
For any preorder, the statement that eventually holds for all larger elements can be equivalently stated as a pointwise eventual property.
Русский
Для любого предела на порядке существует эквивалентное формальное выражение: рано или поздно свойство выполняется по всем большим элементам.
LaTeX
$$$[\text{Preorder } \alpha] \\ (\forall^\infty x \in \operatorname{atTop}, \forall y, x \le y \Rightarrow p(y)) \iff (\forall^\infty x \in \operatorname{atTop}, p(x))$$$
Lean4
theorem eventually_forall_ge_atTop [Preorder α] {p : α → Prop} :
(∀ᶠ x in atTop, ∀ y, x ≤ y → p y) ↔ ∀ᶠ x in atTop, p x :=
by
refine ⟨fun h ↦ h.mono fun x hx ↦ hx x le_rfl, fun h ↦ ?_⟩
rcases (hasBasis_iInf_principal_finite _).eventually_iff.1 h with ⟨S, hSf, hS⟩
refine mem_iInf_of_iInter hSf (V := fun x ↦ Ici x.1) (fun _ ↦ Subset.rfl) fun x hx y hy ↦ ?_
simp only [mem_iInter] at hS hx
exact hS fun z hz ↦ le_trans (hx ⟨z, hz⟩) hy
