Lean4
instance [ts : TopologicalSpace ι] [ht : OrderTopology ι] [SecondCountableTopology ι] :
SecondCountableTopology (WithTop ι) := by
classical
rcases isEmpty_or_nonempty ι with hι | ⟨⟨x₀⟩⟩
·
infer_instance
/- Let `c` be a countable set in `ι` such that the topology is generated by the sets `Iio a`
and `Ioi a` for `a ∈ c`, by second-countability. Let `c'` be a dense set in `ι`, again by
second-countability. Let `d` in `WithTop ι` be obtained from `c ∪ c'`, by adding `⊤` and a point
`x₁ : ι` with `Ioi x₁ = ∅` if there is one.
We will show that the topology on `WithTop ι` is generated by the intervals `Iio a` and `Ioi a`
for `a ∈ d`, which will conclude the proof by countability of `d`. -/
obtain ⟨c, c_count, hc⟩ : ∃ (c : Set ι), c.Countable ∧ ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a} :=
exists_countable_generateFrom_Ioi_Iio ι
obtain ⟨c', c'_count, hc'⟩ : ∃ c' : Set ι, c'.Countable ∧ Dense c' := SeparableSpace.exists_countable_dense
let x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
let d : Set (WithTop ι) := (↑) '' c ∪ (↑) '' c' ∪ {⊤} ∪ {(x₁ : WithTop ι)}
suffices H : instWithTopOfOrderTopology = generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}
by
refine ⟨{s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}, ?_, by rw [← H]⟩
have d_count : d.Countable := (((c_count.image _).union (c'_count.image _)).union (by simp)).union (by simp)
have : {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} = Ioi '' d ∪ Iio '' d := by ext; simp; grind
rw [this]
exact
(d_count.image _).union
(d_count.image _)
-- We should check the easy direction that all the elements in our generating set are open.
-- This is trivial as these are all intervals.
apply le_antisymm
· apply le_generateFrom_iff_subset_isOpen.2
simp only [setOf_subset_setOf, forall_exists_index, and_imp]
grind [isOpen_Iio', isOpen_Ioi']
/- Now, let us check that our sets indeed generates the topology. As the topology is
generated by the open half-infinite intervals by definition, we should check that open
half-infinite intervals are covered by finite intersections of our sets. -/
let basis : Set (Set ι) :=
{s | ∃ (f g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ (⋂ a ∈ g, Iio a)}
have h_basis : IsTopologicalBasis basis := isTopologicalBasis_biInter_Ioi_Iio_of_generateFrom c hc
rw [OrderTopology.topology_eq_generate_intervals (α := WithTop ι)]
apply le_generateFrom_iff_subset_isOpen.2
simp only [setOf_subset_setOf, forall_exists_index]
rintro u a
(rfl | rfl)
-- Consider an interval of the form `Ioi a`. We should cover it by finite intersections of
-- our sets.
·
induction a with
| top =>
-- for `a = ⊤`, this is trivial as `Ioi ⊤` is in our set by design
apply isOpen_generateFrom_of_mem
exact ⟨⊤, by simp [d]⟩
| coe a =>
-- for `a : ι`, we consider an element `b ∈ Ioi a`, and seek a finite intersection of our
-- sets containing it and contained in `Ioi a`.
rw [@isOpen_iff_forall_mem_open]
intro b hb
induction b with
| top =>
-- if `b = ⊤`, then either `Ioi a` is empty in `ι` and then we use `Ioi (↑x₁)` which is
-- in our set and reduced to `⊤`
rcases eq_empty_or_nonempty (Ioi a) with ha | ha
· refine ⟨Ioi x₁, ?_, ?_, by simp⟩
· have : Ioi x₁ = ∅ := by
have h : ∃ x, Ioi x = ∅ := ⟨a, ha⟩
simp only [x₁, h, ↓reduceDIte]
exact h.choose_spec
simp [WithTop.Ioi_coe, this]
· apply isOpen_generateFrom_of_mem
simp [d]
-- If `Ioi a` is not empty in `ι`, it contains a point `b` in the dense set `c'`, and then
-- we use `Ioi (↑b)` which is in our set, contained in `Ioi (↑a)` and contains `⊤`.
· obtain ⟨b, bc', hb⟩ : ∃ b ∈ c', b ∈ Ioi a := hc'.exists_mem_open (isOpen_Ioi' a) ha
refine ⟨Ioi b, ?_, ?_, by simp⟩
· apply Ioi_subset_Ioi
simpa using hb.le
· apply isOpen_generateFrom_of_mem
exact ⟨b, by simp [d, bc'], Or.inl rfl⟩
| coe b =>
-- if `b` comes from `ι`, then in `ι` we can find a finite intersection of our sets
-- containing `b` and contained in `Ioi a`. We lift it to `WithTop ι`.
simp only [mem_Ioi, WithTop.coe_lt_coe] at hb
obtain ⟨t, ⟨f, g, hfc, hgc, f_fin, g_fin, rfl⟩, hb, hfg⟩ : ∃ t ∈ basis, b ∈ t ∧ t ⊆ Ioi a :=
h_basis.isOpen_iff.1 (isOpen_Ioi' a) b hb
refine ⟨(⋂ z ∈ f, Ioi z) ∩ ⋂ z ∈ g, Iio z, ?_, ?_, by simpa using hb⟩
· intro w hw
induction w with
| top => simp
| coe w =>
simp only [mem_Ioi, WithTop.coe_lt_coe]
apply hfg
simpa using hw
· apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
· apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
· exact f_fin
· intro i hi
apply isOpen_generateFrom_of_mem
simp [d]
grind
· apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
· exact g_fin
· intro i hi
apply isOpen_generateFrom_of_mem
simp [d]
grind
-- Consider an interval of the form `Iio a`. We should cover it by finite intersections of
-- our sets.
·
induction a with
| top =>
-- for `a = ⊤`, this is trivial as `Iio ⊤` is in our set by design
apply isOpen_generateFrom_of_mem
exact ⟨⊤, by simp [d]⟩
| coe a =>
-- for `a : ι`, we consider an element `b ∈ Iio a`, and seek a finite intersection of our
-- sets containing it and contained in `Iio a`.
rw [@isOpen_iff_forall_mem_open]
intro b hb
induction b with
| top => simp at hb
| coe b =>
-- `b` can not be equal to `⊤`, so it comes from `ι`. In `ι` we can find a finite
-- intersection of our sets containing `b` and contained in `Iio a`. We lift it
-- to `WithTop ι`, and intersect with `Iio ⊤` (which is also in our set) to exclude `⊤`.
simp only [mem_Iio, WithTop.coe_lt_coe] at hb
obtain ⟨t, ⟨f, g, hfc, hgc, f_fin, g_fin, rfl⟩, hb, hfg⟩ : ∃ t ∈ basis, b ∈ t ∧ t ⊆ Iio a :=
h_basis.isOpen_iff.1 (isOpen_Iio' a) b hb
refine ⟨(⋂ z ∈ f, Ioi z) ∩ (⋂ z ∈ g, Iio z) ∩ Iio ⊤, ?_, ?_, by simpa using hb⟩
· intro w hw
induction w with
| top => simp at hw
| coe w =>
simp only [mem_Iio, WithTop.coe_lt_coe]
apply hfg
simpa using hw
· apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}); swap
· apply isOpen_generateFrom_of_mem
simp [d]
apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
· apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
· exact f_fin
· intro i hi
apply isOpen_generateFrom_of_mem
simp [d]
grind
· apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
· exact g_fin
· intro i hi
apply isOpen_generateFrom_of_mem
simp [d]
grind
