English
Let p be a property on α with directed order and nonempty domain. The predicate p holds frequently along atBot if and only if for every a, there exists b ≤ a with p(b).
Русский
Пусть p — свойство на α с направленным порядком и непустым множеством значений. Свойство p встречается часто в направлении atBot тогда и только если для каждого a существует b ≤ a such that p(b).
LaTeX
$$$(\exists\!\text{freq} x\ in\ atBot, p x) \leftrightarrow \forall a, \exists b \le a, p b$$$
Lean4
theorem frequently_atBot : (∃ᶠ x in atBot, p x) ↔ ∀ a, ∃ b ≤ a, p b :=
frequently_atTop (α := αᵒᵈ)