English
In an OrderTopology α with NoMaxOrder and NoMinOrder, a set s is a neighborhood of a iff there exist l<u with a∈Ioo(l,u) and Ioo(l,u)⊆s.
Русский
В OrderTopology α с отсутствием максимума и минимума, s ∈ nhds(a) тогда и только тогда, когда существуют l<u с a∈Ioo(l,u) и Ioo(l,u)⊆s.
LaTeX
$$$s\\in \\nhds a \\iff \\exists l,u\\, (a\\in Ioo(l,u) \\land Ioo(l,u)\\subseteq s)$$$
Lean4
theorem topology_eq_generateFrom [OrderTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) :
‹TopologicalSpace α› = .generateFrom (Ioi '' s ∪ Iio '' s) :=
by
refine (OrderTopology.topology_eq_generate_intervals (α := α)).trans ?_
refine le_antisymm (generateFrom_anti ?_) (le_generateFrom ?_)
· simp only [union_subset_iff, image_subset_iff]
exact ⟨fun a _ ↦ ⟨a, .inl rfl⟩, fun a _ ↦ ⟨a, .inr rfl⟩⟩
· rintro _ ⟨a, rfl | rfl⟩
· rw [hs.Ioi_eq_biUnion]
let _ := generateFrom (Ioi '' s ∪ Iio '' s)
exact isOpen_iUnion fun x ↦ isOpen_iUnion fun h ↦ .basic _ <| .inl <| mem_image_of_mem _ h.1
· rw [hs.Iio_eq_biUnion]
let _ := generateFrom (Ioi '' s ∪ Iio '' s)
exact isOpen_iUnion fun x ↦ isOpen_iUnion fun h ↦ .basic _ <| .inr <| mem_image_of_mem _ h.1
