English
Let p be a predicate on pairs from a nonempty directed preorder with bottom, i.e. on α × α. Then p holds eventually along the bottom filter if and only if there exists a bound a such that p(k, l) holds for all k, l ≤ a.
Русский
Пусть p — предикат на пары элементов из направленного непустого порядка с наименьшей гранью, т.е. на α × α. Тогда свойство p выполняется вплоть до нижнего фильтра тогда, когда существует предел a, такой что для всех k, l ≤ a выполняется p(k, l).
LaTeX
$$$ (\forall^\infty x \in \mathrm{atBot},\ p(x)) \iff \exists a, \forall k \le a, \forall l \le a,\ p(k,l) $$$
Lean4
theorem eventually_atBot_prod_self' [Nonempty α] [Preorder α] [IsDirected α (· ≥ ·)] {p : α × α → Prop} :
(∀ᶠ x in atBot, p x) ↔ ∃ a, ∀ k ≤ a, ∀ l ≤ a, p (k, l) := by
simp only [eventually_atBot_prod_self, forall_cond_comm]
