English
For Nonempty α with Preorder and IsDirected (≤), an eventual property on pairs is equivalent to existence of a common upper bound a such that p(k,l) holds for all k,l ≥ a.
Русский
Для непустого α с предикатом упорядочивания и направленности: свойство, выполняемое часто для пары, эквивалентно существованию общего верхнего предела a, такого что p(k,l) выполняется для всех k,l ≥ a.
LaTeX
$$Для α: Nonempty, Preorder α, IsDirected α (≤): $(\\forall^\\infty x \\in \\operatorname{atTop}, p x) \\iff \\exists a, \\forall k l, a ≤ k \\rightarrow a ≤ l \\rightarrow p {fst:=k, snd:=l}$$$
Lean4
theorem eventually_atTop_prod_self [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)] {p : α × α → Prop} :
(∀ᶠ x in atTop, p x) ↔ ∃ a, ∀ k l, a ≤ k → a ≤ l → p (k, l) :=
eventually_atBot_prod_self (α := αᵒᵈ)
