frequently_gt_nhds — Mathlib

English

Let α be a topological space with a preorder. If the upper-left neighborhood 𝓝[>] a is nontrivial, then there are frequently points x in 𝓝 a with a < x.

Русский

Пусть α — топологическое пространство с предельным порядком. Если фильтр ближайших точек слева выше a, 𝓝[>] a, ненулевой, то часто встречаются точки x ∈ 𝓝 a такие что a < x.

LaTeX

$$$[\mathrm{NeBot} (\mathcal{N}_{[>]} a)] \Rightarrow \existsᶠ x \in 𝓝 a, a < x$$$

Lean4

theorem frequently_gt_nhds (a : α) [NeBot (𝓝[>] a)] : ∃ᶠ x in 𝓝 a, a < x :=
  frequently_iff_neBot.2 ‹_›

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