frequently_lt_nhds — Mathlib

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 ‹_›

Похожие утверждения