English
If a predicate p on α × β holds eventually in atBot for pairs, then it holds eventually in both coordinates: there is a stage after which for every k and then for every l (both in atBot) p(k, l) holds.
Русский
Если предикат p на α × β выполняется вплоть до бесконечности по направлению вниз на пары, то он выполняется вплоть до бесконечности по всем парам координат: существует этап, после которого для каждого k и затем для каждого l (оба в atBot) выполняется p(k, l).
LaTeX
$$$ (\forall^\infty x \in \mathrm{atBot},\ p(x)) \Rightarrow (\forall^\infty k \in \mathrm{atBot},\ \forall^\infty l \in \mathrm{atBot},\ p(k,l)) $$$
Lean4
theorem eventually_atBot_curry [Preorder α] [Preorder β] {p : α × β → Prop} (hp : ∀ᶠ x : α × β in Filter.atBot, p x) :
∀ᶠ k in atBot, ∀ᶠ l in atBot, p (k, l) :=
@eventually_atTop_curry αᵒᵈ βᵒᵈ _ _ _ hp
