English
Let α be a topological space equipped with a preorder. If there are points strictly below a accumulating at a (i.e., the left-neighborhood filter 𝓝[<] a is nontrivial), then there are frequently points x in the neighborhood 𝓝 a with x < a.
Русский
Пусть α — топологическое пространство с пределовым порядком. Если существуют точки строго меньше a, сходящиеся к a (непустен фильтр 𝓝[<] a), то в окрестности 𝓝 a часто встречаются точки x < a.
LaTeX
$$$[\mathrm{NeBot} (\mathcal{N}_{[<]} a)] \Rightarrow \existsᶠ x \in 𝓝 a, x < a$$$
Lean4
theorem frequently_lt_nhds (a : α) [NeBot (𝓝[<] a)] : ∃ᶠ x in 𝓝 a, x < a :=
frequently_iff_neBot.2 ‹_›