English
In a second-countable ordered space, the topology is generated by a countable family of half-infinite intervals Ioi and Iio.
Русский
Во втором счётном упорядоченном 공간 топология задаётся счётной семейством полупрямых интервалов Ioi и Iio.
LaTeX
$$$\\exists c\\subseteq \\alpha, c\\text{ countable} \\land \\mathcal{T}=generateFrom\\{s\\mid \\exists a\\in c, s=Ioi(a)\\lor s=Iio(a)\\}$$$
Lean4
/-- In a second countable topological space with the order topology, the topology is generated
by half-infinite open intervals with endpoints in a countable set. -/
theorem exists_countable_generateFrom_Ioi_Iio [OrderTopology α] [SecondCountableTopology α] :
∃ (c : Set α), c.Countable ∧ ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a} :=
by
rcases isEmpty_or_nonempty α with hα | hα
· exact ⟨∅, by simp, Subsingleton.elim _ _⟩
obtain ⟨t, t_subs, t_count, ht⟩ : ∃ t ⊆ {s | ∃ a, s = Ioi a ∨ s = Iio a}, t.Countable ∧ ts = generateFrom t :=
exists_countable_of_generateFrom OrderTopology.topology_eq_generate_intervals
have A : ∀ s ∈ t, ∃ a, s = Ioi a ∨ s = Iio a := t_subs
choose! a ha using A
refine ⟨a '' t, t_count.image _, ?_⟩
apply le_antisymm
· apply le_generateFrom_iff_subset_isOpen.2
simp only [mem_image, exists_exists_and_eq_and, setOf_subset_setOf, forall_exists_index, and_imp]
grind [isOpen_Iio', isOpen_Ioi']
· rw [ht]
apply generateFrom_anti
intro s hs
simp only [mem_image, exists_exists_and_eq_and, mem_setOf_eq]
grind
