English
In any nontrivial densely ordered topological space with the order topology, every point x is the limit of other points; equivalently, there exist points y ≠ x arbitrarily close to x.
Русский
В ненулевом плотном линейно упорядоченном топологическом пространстве с топологией порядка каждая точка x является пределом других точек; то есть существуют точки y ≠ x, приближающиеся к x.
LaTeX
$$$\\forall x, \\mathcal{N}_{x}^{\\neq} \\neq \\bot$, i.e. there exist points $y \\neq x$ arbitrarily close to $x$.$$
Lean4
instance (x : α) [Nontrivial α] : NeBot (𝓝[≠] x) :=
by
refine forall_mem_nonempty_iff_neBot.1 fun s hs => ?_
obtain ⟨u, u_open, xu, us⟩ : ∃ u : Set α, IsOpen u ∧ x ∈ u ∧ u ∩ { x }ᶜ ⊆ s := mem_nhdsWithin.1 hs
obtain ⟨a, b, a_lt_b, hab⟩ : ∃ a b : α, a < b ∧ Ioo a b ⊆ u := u_open.exists_Ioo_subset ⟨x, xu⟩
obtain ⟨y, hy⟩ : ∃ y, a < y ∧ y < b := exists_between a_lt_b
rcases ne_or_eq x y with (xy | rfl)
· exact ⟨y, us ⟨hab hy, xy.symm⟩⟩
obtain ⟨z, hz⟩ : ∃ z, a < z ∧ z < x := exists_between hy.1
exact ⟨z, us ⟨hab ⟨hz.1, hz.2.trans hy.2⟩, hz.2.ne⟩⟩
