.lake/packages/mathlib/Mathlib/Topology/Bases.lean

1/-

3Released under Apache 2.0 license as described in the file LICENSE.

4Authors: Johannes Hölzl, Mario Carneiro

5-/

6module

8public import Mathlib.Data.Set.Constructions

9public import Mathlib.Order.Filter.AtTopBot.CountablyGenerated

10public import Mathlib.Topology.Constructions

11public import Mathlib.Topology.ContinuousOn

12public import Mathlib.Topology.NhdsWithin

14/-!

15# Bases of topologies. Countability axioms.

17A topological basis on a topological space `t` is a collection of sets,

18such that all open sets can be generated as unions of these sets, without the need to take

19finite intersections of them. This file introduces a framework for dealing with these collections,

20and also what more we can say under certain countability conditions on bases,

21which are referred to as first- and second-countable.

22We also briefly cover the theory of separable spaces, which are those with a countable, dense

23subset. If a space is second-countable, and also has a countably generated uniformity filter

24(for example, if `t` is a metric space), it will automatically be separable (and indeed, these

25conditions are equivalent in this case).

27## Main definitions

29* `TopologicalSpace.IsTopologicalBasis s`: The topological space `t` has basis `s`.

30* `TopologicalSpace.SeparableSpace α`: The topological space `t` has a countable, dense subset.

31* `TopologicalSpace.IsSeparable s`: The set `s` is contained in the closure of a countable set.

32* `FirstCountableTopology α`: A topology in which `𝓝 x` is countably generated for

33 every `x`.

34* `SecondCountableTopology α`: A topology which has a topological basis which is

35 countable.

37## Main results

39* `MapClusterPt.tendsto_subseq`: In a first-countable space, cluster points are limits of

40 subsequences.

41* `TopologicalSpace.SecondCountableTopology.isOpen_iUnion_countable`: In a second-countable space,

42 the union of arbitrarily-many open sets is equal to a sub-union of only countably many of these

43 sets.

44* `TopologicalSpace.SecondCountableTopology.countable_cover_nhds`: Consider `f : α → Set α` with the

45 property that `f x ∈ 𝓝 x` for all `x`. Then there is some countable set `s` whose image covers

46 the space.

48## Implementation Notes

49For our applications we are interested in the existence of a countable basis, but we do not need the

50concrete basis itself. This allows us to declare these type classes as `Prop` to use them as mixins.

52## TODO

54More fine grained instances for `FirstCountableTopology`,

55`TopologicalSpace.SeparableSpace`, and more.

56-/

58@[expose] public section

60open Set Filter Function Topology

62noncomputable section

64namespace TopologicalSpace

66universe u

68variable {α : Type u} {β : Type*} [t : TopologicalSpace α] {B : Set (Set α)} {s : Set α}

70/-- A topological basis is one that satisfies the necessary conditions so that

71 it suffices to take unions of the basis sets to get a topology (without taking

72 finite intersections as well). -/

73structure IsTopologicalBasis (s : Set (Set α)) : Prop where

74 /-- For every point `x`, the set of `t ∈ s` such that `x ∈ t` is directed downwards. -/

  exists_subset_inter : ∀ t₁ ∈ s, ∀ t₂ ∈ s, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ s, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

76 /-- The sets from `s` cover the whole space. -/

77 sUnion_eq : ⋃₀ s = univ

78 /-- The topology is generated by sets from `s`. -/

79 eq_generateFrom : t = generateFrom s

81/-- If a family of sets `s` generates the topology, then intersections of finite

82subcollections of `s` form a topological basis. -/

83theorem isTopologicalBasis_of_subbasis {s : Set (Set α)} (hs : t = generateFrom s) :

84 IsTopologicalBasis ((fun f => ⋂₀ f) '' { f : Set (Set α) | f.Finite ∧ f ⊆ s }) := by

85 subst t; let := generateFrom s

86 refine ⟨?_, ?_, le_antisymm (le_generateFrom ?_) <| generateFrom_anti fun t ht => ?_⟩

87 · rintro _ ⟨t₁, ⟨hft₁, ht₁b⟩, rfl⟩ _ ⟨t₂, ⟨hft₂, ht₂b⟩, rfl⟩ x h

88 exact ⟨_, ⟨_, ⟨hft₁.union hft₂, union_subset ht₁b ht₂b⟩, sInter_union t₁ t₂⟩, h, Subset.rfl⟩

89 · rw [sUnion_image, iUnion₂_eq_univ_iff]

90 exact fun x => ⟨∅, ⟨finite_empty, empty_subset _⟩, sInter_empty.substr <| mem_univ x⟩

91 · rintro _ ⟨t, ⟨hft, htb⟩, rfl⟩

92 exact hft.isOpen_sInter fun s hs ↦ GenerateOpen.basic _ <| htb hs

93 · rw [← sInter_singleton t]

94 exact ⟨{t}, ⟨finite_singleton t, singleton_subset_iff.2 ht⟩, rfl⟩

96theorem isTopologicalBasis_of_subbasis_of_finiteInter {s : Set (Set α)} (hsg : t = generateFrom s)

97 (hsi : FiniteInter s) : IsTopologicalBasis s := by

98 convert! isTopologicalBasis_of_subbasis hsg

99 refine le_antisymm (fun t ht ↦ ⟨{t}, by simpa using ht⟩) ?_

100 rintro _ ⟨g, ⟨hg, hgs⟩, rfl⟩

101 lift g to Finset (Set α) using hg

102 exact hsi.finiteInter_mem g hgs

103

104theorem isTopologicalBasis_of_subbasis_of_inter {r : Set (Set α)} (hsg : t = generateFrom r)

105 (hsi : ∀ ⦃s⦄, s ∈ r → ∀ ⦃t⦄, t ∈ r → s ∩ t ∈ r) : IsTopologicalBasis (insert univ r) :=

106 isTopologicalBasis_of_subbasis_of_finiteInter (by simpa using hsg) (FiniteInter.mk₂ hsi)

107

108theorem IsTopologicalBasis.of_hasBasis_nhds {s : Set (Set α)}

109 (h_nhds : ∀ a, (𝓝 a).HasBasis (fun t ↦ t ∈ s ∧ a ∈ t) id) : IsTopologicalBasis s where

110 exists_subset_inter t₁ ht₁ t₂ ht₂ x hx := by

111 simpa only [and_assoc, (h_nhds x).mem_iff]

112 using! (inter_mem ((h_nhds _).mem_of_mem ⟨ht₁, hx.1⟩) ((h_nhds _).mem_of_mem ⟨ht₂, hx.2⟩))

113 sUnion_eq := sUnion_eq_univ_iff.2 fun x ↦ (h_nhds x).ex_mem

114 eq_generateFrom := ext_nhds fun x ↦ by

115 simpa only [nhds_generateFrom, and_comm] using! (h_nhds x).eq_biInf

116

117/-- If a family of open sets `s` is such that every open neighbourhood contains some

118member of `s`, then `s` is a topological basis. -/

119theorem isTopologicalBasis_of_isOpen_of_nhds {s : Set (Set α)} (h_open : ∀ u ∈ s, IsOpen u)

120 (h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u) :

121 IsTopologicalBasis s :=

122 .of_hasBasis_nhds <| fun a ↦

123 (nhds_basis_opens a).to_hasBasis' (by simpa [and_assoc] using h_nhds a)

124 fun _ ⟨hts, hat⟩ ↦ (h_open _ hts).mem_nhds hat

125

126/-- A set `s` is in the neighbourhood of `a` iff there is some basis set `t`, which

127contains `a` and is itself contained in `s`. -/

128theorem IsTopologicalBasis.mem_nhds_iff {a : α} {s : Set α} {b : Set (Set α)}

129 (hb : IsTopologicalBasis b) : s ∈ 𝓝 a ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s := by

130 change s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s

131 rw [hb.eq_generateFrom, nhds_generateFrom, biInf_sets_eq]

132 · simp [and_assoc, and_left_comm]

133 · rintro s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩

134 let ⟨u, hu₁, hu₂, hu₃⟩ := hb.1 _ hs₂ _ ht₂ _ ⟨hs₁, ht₁⟩

135 exact ⟨u, ⟨hu₂, hu₁⟩, le_principal_iff.2 (hu₃.trans inter_subset_left),

136 le_principal_iff.2 (hu₃.trans inter_subset_right)⟩

137 · rcases eq_univ_iff_forall.1 hb.sUnion_eq a with ⟨i, h1, h2⟩

138 exact ⟨i, h2, h1⟩

139

140theorem IsTopologicalBasis.isOpen_iff {s : Set α} {b : Set (Set α)} (hb : IsTopologicalBasis b) :

141 IsOpen s ↔ ∀ a ∈ s, ∃ t ∈ b, a ∈ t ∧ t ⊆ s := by simp [isOpen_iff_mem_nhds, hb.mem_nhds_iff]

142

143theorem IsTopologicalBasis.of_isOpen_of_subset {s s' : Set (Set α)} (h_open : ∀ u ∈ s', IsOpen u)

144 (hs : IsTopologicalBasis s) (hss' : s ⊆ s') : IsTopologicalBasis s' :=

145 isTopologicalBasis_of_isOpen_of_nhds h_open fun a _ ha u_open ↦

146 have ⟨t, hts, ht⟩ := hs.isOpen_iff.mp u_open a ha; ⟨t, hss' hts, ht⟩

147

148theorem IsTopologicalBasis.nhds_hasBasis {b : Set (Set α)} (hb : IsTopologicalBasis b) {a : α} :

149 (𝓝 a).HasBasis (fun t : Set α => t ∈ b ∧ a ∈ t) fun t => t :=

150 ⟨fun s => hb.mem_nhds_iff.trans <| by simp only [and_assoc]⟩

151

152protected theorem IsTopologicalBasis.isOpen {s : Set α} {b : Set (Set α)}

153 (hb : IsTopologicalBasis b) (hs : s ∈ b) : IsOpen s := by

154 rw [hb.eq_generateFrom]

155 exact .basic s hs

156

157theorem IsTopologicalBasis.insert_empty {s : Set (Set α)} (h : IsTopologicalBasis s) :

158 IsTopologicalBasis (insert ∅ s) :=

159 h.of_isOpen_of_subset (by rintro _ (rfl | hu); exacts [isOpen_empty, h.isOpen hu])

160 (subset_insert ..)

161

162theorem IsTopologicalBasis.sdiff_empty {s : Set (Set α)} (h : IsTopologicalBasis s) :

163 IsTopologicalBasis (s \ {∅}) :=

164 isTopologicalBasis_of_isOpen_of_nhds (fun _ hu ↦ h.isOpen hu.1) fun a _ ha hu ↦

165 have ⟨t, hts, ht⟩ := h.isOpen_iff.mp hu a ha

166 ⟨t, ⟨hts, ne_of_mem_of_not_mem' ht.1 <| notMem_empty _⟩, ht⟩

167

168@[deprecated (since := "2026-06-03")]

169alias IsTopologicalBasis.diff_empty := IsTopologicalBasis.sdiff_empty

170

171protected theorem IsTopologicalBasis.mem_nhds {a : α} {s : Set α} {b : Set (Set α)}

172 (hb : IsTopologicalBasis b) (hs : s ∈ b) (ha : a ∈ s) : s ∈ 𝓝 a :=

173 (hb.isOpen hs).mem_nhds ha

174

175theorem IsTopologicalBasis.exists_subset_of_mem_open {b : Set (Set α)} (hb : IsTopologicalBasis b)

176 {a : α} {u : Set α} (au : a ∈ u) (ou : IsOpen u) : ∃ v ∈ b, a ∈ v ∧ v ⊆ u :=

177 hb.mem_nhds_iff.1 <| IsOpen.mem_nhds ou au

178

179theorem IsTopologicalBasis.isTopologicalBasis_of_exists_subset {B B' : Set (Set α)}

180 (hB : IsTopologicalBasis B) (h_open : ∀ u ∈ B', IsOpen u)

181 (h : ∀ u ∈ B, ∀ x ∈ u, ∃ v ∈ B', x ∈ v ∧ v ⊆ u) : IsTopologicalBasis B' := by

182 refine isTopologicalBasis_of_isOpen_of_nhds h_open fun x u hx hu => ?_

183 obtain ⟨w, hwB, hxw, hwu⟩ := hB.exists_subset_of_mem_open hx hu

184 obtain ⟨v, hvB', hxv, hvw⟩ := h w hwB x hxw

185 exact ⟨v, hvB', hxv, hvw.trans hwu⟩

186

187/-- Any open set is the union of the basis sets contained in it. -/

188theorem IsTopologicalBasis.open_eq_sUnion' {B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α}

189 (ou : IsOpen u) : u = ⋃₀ { s ∈ B | s ⊆ u } :=

190 ext fun _a =>

191 ⟨fun ha =>

192 let ⟨b, hb, ab, bu⟩ := hB.exists_subset_of_mem_open ha ou

193 ⟨b, ⟨hb, bu⟩, ab⟩,

194 fun ⟨_b, ⟨_, bu⟩, ab⟩ => bu ab⟩

195

196theorem IsTopologicalBasis.open_eq_sUnion {B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α}

197 (ou : IsOpen u) : ∃ S ⊆ B, u = ⋃₀ S :=

198 ⟨{ s ∈ B | s ⊆ u }, fun _ h => h.1, hB.open_eq_sUnion' ou⟩

199

200theorem IsTopologicalBasis.open_iff_eq_sUnion {B : Set (Set α)} (hB : IsTopologicalBasis B)

201 {u : Set α} : IsOpen u ↔ ∃ S ⊆ B, u = ⋃₀ S :=

202 ⟨hB.open_eq_sUnion, fun ⟨_S, hSB, hu⟩ => hu.symm ▸ isOpen_sUnion fun _s hs => hB.isOpen (hSB hs)⟩

203

204theorem IsTopologicalBasis.open_eq_iUnion {B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α}

205 (ou : IsOpen u) : ∃ (β : Type u) (f : β → Set α), (u = ⋃ i, f i) ∧ ∀ i, f i ∈ B :=

206 ⟨↥({ s ∈ B | s ⊆ u }), (↑), by

207 rw [← sUnion_eq_iUnion]

208 apply hB.open_eq_sUnion' ou, fun s => And.left s.2⟩

209

210@[elab_as_elim]

211lemma IsTopologicalBasis.isOpen_induction {P : Set α → Prop} (hB : IsTopologicalBasis B)

212 (basis : ∀ b ∈ B, P b) (sUnion : ∀ S, (∀ s ∈ S, P s) → P (⋃₀ S)) {s : Set α} (hs : IsOpen s) :

213 P s := by

214 obtain ⟨S, hS, rfl⟩ := hB.open_eq_sUnion hs; exact sUnion _ fun b hb ↦ basis _ <| hS hb

215

216lemma IsTopologicalBasis.subset_of_forall_subset {t : Set α} (hB : IsTopologicalBasis B)

217 (hs : IsOpen s) (h : ∀ U ∈ B, U ⊆ s → U ⊆ t) : s ⊆ t := by

218 rw [hB.open_eq_sUnion' hs]; simpa [sUnion_subset_iff]

219

220lemma IsTopologicalBasis.eq_of_forall_subset_iff {t : Set α} (hB : IsTopologicalBasis B)

221 (hs : IsOpen s) (ht : IsOpen t) (h : ∀ U ∈ B, U ⊆ s ↔ U ⊆ t) : s = t := by

222 rw [hB.open_eq_sUnion' hs, hB.open_eq_sUnion' ht]

223 exact congr_arg _ (Set.ext fun U ↦ and_congr_right <| h _)

224

225/-- A point `a` is in the closure of `s` iff all basis sets containing `a` intersect `s`. -/

226theorem IsTopologicalBasis.mem_closure_iff {b : Set (Set α)} (hb : IsTopologicalBasis b) {s : Set α}

227 {a : α} : a ∈ closure s ↔ ∀ o ∈ b, a ∈ o → (o ∩ s).Nonempty :=

228 (mem_closure_iff_nhds_basis' hb.nhds_hasBasis).trans <| by simp only [and_imp]

229

230/-- A set is dense iff it has non-trivial intersection with all basis sets. -/

231theorem IsTopologicalBasis.dense_iff {b : Set (Set α)} (hb : IsTopologicalBasis b) {s : Set α} :

232 Dense s ↔ ∀ o ∈ b, Set.Nonempty o → (o ∩ s).Nonempty := by

233 simp only [Dense, hb.mem_closure_iff]

234 exact ⟨fun h o hb ⟨a, ha⟩ => h a o hb ha, fun h a o hb ha => h o hb ⟨a, ha⟩⟩

235

236theorem IsTopologicalBasis.isOpenMap_iff [TopologicalSpace β] {B : Set (Set α)}

237 (hB : IsTopologicalBasis B) {f : α → β} : IsOpenMap f ↔ ∀ s ∈ B, IsOpen (f '' s) := by

238 refine ⟨fun H o ho => H _ (hB.isOpen ho), fun hf o ho => ?_⟩

239 rw [hB.open_eq_sUnion' ho, sUnion_eq_iUnion, image_iUnion]

240 exact isOpen_iUnion fun s => hf s s.2.1

241

242theorem IsTopologicalBasis.exists_nonempty_subset {B : Set (Set α)} (hb : IsTopologicalBasis B)

243 {u : Set α} (hu : u.Nonempty) (ou : IsOpen u) : ∃ v ∈ B, Set.Nonempty v ∧ v ⊆ u :=

244 let ⟨x, hx⟩ := hu

245 let ⟨v, vB, xv, vu⟩ := hb.exists_subset_of_mem_open hx ou

246 ⟨v, vB, ⟨x, xv⟩, vu⟩

247

248theorem isTopologicalBasis_opens : IsTopologicalBasis { U : Set α | IsOpen U } :=

249 isTopologicalBasis_of_isOpen_of_nhds (by tauto) (by tauto)

250

251protected lemma _root_.Topology.IsInducing.isTopologicalBasis [TopologicalSpace β] {f : α → β}

252 (hf : IsInducing f) {T : Set (Set β)} (h : IsTopologicalBasis T) :

253 IsTopologicalBasis ((preimage f) '' T) :=

254 .of_hasBasis_nhds fun a ↦ by

255 convert! (hf.basis_nhds (h.nhds_hasBasis (a := f a))).to_image_id with s

256 aesop

257

258@[deprecated Topology.IsInducing.isTopologicalBasis (since := "2026-08-21")]

259protected lemma IsTopologicalBasis.isInducing [TopologicalSpace β] {f : α → β} {T : Set (Set β)}

260 (hf : IsInducing f) (h : IsTopologicalBasis T) : IsTopologicalBasis ((preimage f) '' T) :=

261 hf.isTopologicalBasis h

262

263protected theorem IsTopologicalBasis.induced {α} [s : TopologicalSpace β] (f : α → β)

264 {T : Set (Set β)} (h : IsTopologicalBasis T) :

265 IsTopologicalBasis (t := induced f s) ((preimage f) '' T) :=

266 IsInducing.induced f |>.isTopologicalBasis h (t := induced f s)

267

268protected theorem IsTopologicalBasis.inf {t₁ t₂ : TopologicalSpace β} {B₁ B₂ : Set (Set β)}

269 (h₁ : IsTopologicalBasis (t := t₁) B₁) (h₂ : IsTopologicalBasis (t := t₂) B₂) :

270 IsTopologicalBasis (t := t₁ ⊓ t₂) (image2 (· ∩ ·) B₁ B₂) := by

271 refine .of_hasBasis_nhds (t := ?_) fun a ↦ ?_

272 rw [nhds_inf (t₁ := t₁)]

273 convert! ((h₁.nhds_hasBasis (t := t₁)).inf (h₂.nhds_hasBasis (t := t₂))).to_image_id

274 aesop

275

276theorem IsTopologicalBasis.inf_induced {γ} [s : TopologicalSpace β] {B₁ : Set (Set α)}

277 {B₂ : Set (Set β)} (h₁ : IsTopologicalBasis B₁) (h₂ : IsTopologicalBasis B₂) (f₁ : γ → α)

278 (f₂ : γ → β) :

279

    IsTopologicalBasis (t := induced f₁ t ⊓ induced f₂ s) (image2 (f₁ ⁻¹' · ∩ f₂ ⁻¹' ·) B₁ B₂) := by

280 simpa only [image2_image_left, image2_image_right] using (h₁.induced f₁).inf (h₂.induced f₂)

281

282protected theorem IsTopologicalBasis.prod [TopologicalSpace β] {B₁ : Set (Set α)}

283 {B₂ : Set (Set β)} (h₁ : IsTopologicalBasis B₁) (h₂ : IsTopologicalBasis B₂) :

284 IsTopologicalBasis (image2 (· ×ˢ ·) B₁ B₂) :=

285 h₁.inf_induced h₂ Prod.fst Prod.snd

286

287theorem isTopologicalBasis_of_cover {ι} {U : ι → Set α} (Uo : ∀ i, IsOpen (U i))

288 (Uc : ⋃ i, U i = univ) {b : ∀ i, Set (Set (U i))} (hb : ∀ i, IsTopologicalBasis (b i)) :

289 IsTopologicalBasis (⋃ i : ι, image ((↑) : U i → α) '' b i) := by

290 refine isTopologicalBasis_of_isOpen_of_nhds (fun u hu => ?_) ?_

291 · simp only [mem_iUnion, mem_image] at hu

292 rcases hu with ⟨i, s, sb, rfl⟩

293 exact (Uo i).isOpenMap_subtype_val _ ((hb i).isOpen sb)

294 · intro a u ha uo

295 rcases iUnion_eq_univ_iff.1 Uc a with ⟨i, hi⟩

296 lift a to ↥(U i) using hi

297 rcases (hb i).exists_subset_of_mem_open ha (uo.preimage continuous_subtype_val) with

298 ⟨v, hvb, hav, hvu⟩

299 exact ⟨(↑) '' v, mem_iUnion.2 ⟨i, mem_image_of_mem _ hvb⟩, mem_image_of_mem _ hav,

300 image_subset_iff.2 hvu⟩

301

302protected theorem IsTopologicalBasis.continuous_iff [TopologicalSpace β]

303 {B : Set (Set β)} (hB : IsTopologicalBasis B) {f : α → β} :

304 Continuous f ↔ ∀ s ∈ B, IsOpen (f ⁻¹' s) := by

305 rw [hB.eq_generateFrom, continuous_generateFrom_iff]

306

307theorem IsTopologicalBasis.continuousOn_iff [TopologicalSpace β]

308 {B : Set (Set β)} (hB : IsTopologicalBasis B) {f : α → β} :

309 ContinuousOn f s ↔ ∀ t ∈ B, ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s := by

310 rw [continuousOn_iff']

311 refine ⟨fun h t ht => h t (hB.isOpen ht), fun h t ht => ?_⟩

312 obtain ⟨ι, g, rfl, hg⟩ := hB.open_eq_iUnion ht

313 choose v hv he using (fun i => h (g i) (hg i))

314 exact ⟨⋃ i, v i, isOpen_iUnion hv, by simp_all [iUnion_inter]⟩

315

316@[simp] lemma isTopologicalBasis_empty : IsTopologicalBasis (∅ : Set (Set α)) ↔ IsEmpty α where

317 mp h := by simpa using h.sUnion_eq.symm

318 mpr h := ⟨by simp, by simp [Set.univ_eq_empty_iff.2], Subsingleton.elim ..⟩

319

320@[simp]

321lemma isTopologicalBasis_singleton_empty : IsTopologicalBasis {(∅ : Set α)} ↔ IsEmpty α where

322 mp h := by simpa using h.sdiff_empty

323 mpr h := ⟨by simp, by simp [Set.univ_eq_empty_iff.2], Subsingleton.elim ..⟩

324

325/-- For a topological basis `B`, the finite unions of sets in `B` also form a topological basis. -/

326lemma IsTopologicalBasis.finite_sUnion (hB : IsTopologicalBasis B) :

327 IsTopologicalBasis (sUnion '' {f : Set (Set α) | f.Finite ∧ f ⊆ B}) := by

328 refine hB.of_isOpen_of_subset ?_ (fun u hu ↦ ⟨{u}, by simpa⟩)

329 rintro - ⟨f, ⟨hf1, hf2⟩, rfl⟩

330 exact isOpen_sUnion fun u hu ↦ hB.isOpen (hf2 hu)

331

332variable (α)

333

334/-- A separable space is one with a countable dense subset, available through

335`TopologicalSpace.exists_countable_dense`. If `α` is also known to be nonempty, then

336`TopologicalSpace.denseSeq` provides a sequence `ℕ → α` with dense range, see

337`TopologicalSpace.denseRange_denseSeq`.

338

339If `α` is a uniform space with countably generated uniformity filter (e.g., an `EMetricSpace`), then

340this condition is equivalent to `SecondCountableTopology α`. In this case the

341latter should be used as a typeclass argument in theorems because Lean can automatically deduce

342`TopologicalSpace.SeparableSpace` from `SecondCountableTopology` using

343`TopologicalSpace.SecondCountableTopology.to_separableSpace`, but deducing

344`SecondCountableTopology` from `TopologicalSpace.SeparableSpace` requires more assumptions.

345-/

346@[mk_iff] class SeparableSpace : Prop where

347 /-- There exists a countable dense set. -/

348 exists_countable_dense : ∃ s : Set α, s.Countable ∧ Dense s

349

350theorem exists_countable_dense [SeparableSpace α] : ∃ s : Set α, s.Countable ∧ Dense s :=

351 SeparableSpace.exists_countable_dense

352

353variable {α} in

354theorem exists_countable_dense_subset (s : Set α) [SeparableSpace s] :

355 ∃ t : Set α, t.Countable ∧ t ⊆ s ∧ s ⊆ closure t := by

356 obtain ⟨t, ct, dt⟩ := exists_countable_dense s

357 exact ⟨Subtype.val '' t, ct.image _, by simp, fun x hx ↦ closure_subtype.1 (dt ⟨x, hx⟩)⟩

358

359/-- A nonempty separable space admits a sequence with dense range. Instead of running `cases` on the

360conclusion of this lemma, you might want to use `TopologicalSpace.denseSeq` and

361`TopologicalSpace.denseRange_denseSeq`.

362

363If `α` might be empty, then `TopologicalSpace.exists_countable_dense` is the main way to use

364separability of `α`. -/

365theorem exists_dense_seq [SeparableSpace α] [Nonempty α] : ∃ u : ℕ → α, DenseRange u := by

366 obtain ⟨s : Set α, hs, s_dense⟩ := exists_countable_dense α

367 obtain ⟨u, hu⟩ := Set.countable_iff_exists_subset_range.mp hs

368 exact ⟨u, s_dense.mono hu⟩

369

370/-- A dense sequence in a non-empty separable topological space.

371

372If `α` might be empty, then `TopologicalSpace.exists_countable_dense` is the main way to use

373separability of `α`. -/

374def denseSeq [SeparableSpace α] [Nonempty α] : ℕ → α :=

375 Classical.choose (exists_dense_seq α)

376

377/-- The sequence `TopologicalSpace.denseSeq α` has dense range. -/

378@[simp]

379theorem denseRange_denseSeq [SeparableSpace α] [Nonempty α] : DenseRange (denseSeq α) :=

380 Classical.choose_spec (exists_dense_seq α)

381

382variable {α}

383

384instance (priority := 100) Countable.to_separableSpace [Countable α] : SeparableSpace α where

385 exists_countable_dense := ⟨Set.univ, Set.countable_univ, dense_univ⟩

386

387/-- If `f` has a dense range and its domain is countable, then its codomain is a separable space.

388See also `DenseRange.separableSpace`. -/

389theorem SeparableSpace.of_denseRange {ι : Sort _} [Countable ι] (u : ι → α) (hu : DenseRange u) :

390 SeparableSpace α :=

391 ⟨⟨range u, countable_range u, hu⟩⟩

392

393alias _root_.DenseRange.separableSpace' := SeparableSpace.of_denseRange

394

395/-- If `α` is a separable space and `f : α → β` is a continuous map with dense range, then `β` is

396a separable space as well. E.g., the completion of a separable uniform space is separable. -/

397protected theorem _root_.DenseRange.separableSpace [SeparableSpace α] [TopologicalSpace β]

398 {f : α → β} (h : DenseRange f) (h' : Continuous f) : SeparableSpace β :=

399 let ⟨s, s_cnt, s_dense⟩ := exists_countable_dense α

400 ⟨⟨f '' s, Countable.image s_cnt f, h.dense_image h' s_dense⟩⟩

401

402theorem _root_.Topology.IsQuotientMap.separableSpace [SeparableSpace α] [TopologicalSpace β]

403 {f : α → β} (hf : IsQuotientMap f) : SeparableSpace β :=

404 hf.surjective.denseRange.separableSpace hf.continuous

405

406theorem _root_.IsOpenMap.separableSpace_of_isInducing [TopologicalSpace β] [SeparableSpace β]

407 {f : α → β} (h : IsOpenMap f) (h' : IsInducing f) : SeparableSpace α := by

408 cases isEmpty_or_nonempty α

409 · infer_instance

410 obtain ⟨s, s_cnt, s_dense⟩ := exists_countable_dense β

411 refine ⟨f.invFun '' s, s_cnt.image _, ?_⟩

412 simp_rw [h'.dense_iff, mem_closure_iff]

413 intro x U hU hx

414 obtain ⟨-, ⟨hx'U, x', rfl⟩, hx's⟩ :=

415 s_dense.inter_open_nonempty (U ∩ range f) (hU.inter h.isOpen_range) ⟨f x, hx, mem_range_self _⟩

416 refine ⟨f <| f.invFun <| f x', ?_, mem_image_of_mem _ <| mem_image_of_mem _ hx's⟩

417 rwa [Function.apply_invFun_apply (f := f)]

418

419theorem _root_.IsOpenMap.separableSpace_of_injective [TopologicalSpace β] [SeparableSpace β]

420 {f : α → β} (h : IsOpenMap f) (h' : Function.Injective f) : SeparableSpace α :=

421 let ⟨s, s_cnt, s_dense⟩ := exists_countable_dense β

422 ⟨f ⁻¹' s, s_cnt.preimage h', s_dense.preimage h⟩

423

424theorem _root_.Topology.IsOpenEmbedding.separableSpace [TopologicalSpace β] [SeparableSpace β]

425 {f : α → β} (h : IsOpenEmbedding f) : SeparableSpace α :=

426 h.isOpenMap.separableSpace_of_injective h.injective

427

428/-- The product of two separable spaces is a separable space. -/

429instance [TopologicalSpace β] [SeparableSpace α] [SeparableSpace β] : SeparableSpace (α × β) := by

430 rcases exists_countable_dense α with ⟨s, hsc, hsd⟩

431 rcases exists_countable_dense β with ⟨t, htc, htd⟩

432 exact ⟨⟨s ×ˢ t, hsc.prod htc, hsd.prod htd⟩⟩

433

434/-- The product of a countable family of separable spaces is a separable space. -/

435instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, SeparableSpace (X i)]

436 [Countable ι] : SeparableSpace (∀ i, X i) := by

437 choose t htc htd using (exists_countable_dense <| X ·)

438 have := fun i ↦ (htc i).to_subtype

439 nontriviality ∀ i, X i; inhabit ∀ i, X i

440 classical

441 set f : (Σ I : Finset ι, ∀ i : I, t i) → ∀ i, X i := fun ⟨I, g⟩ i ↦

442 if hi : i ∈ I then g ⟨i, hi⟩ else (default : ∀ i, X i) i

443 refine ⟨⟨range f, countable_range f, dense_iff_inter_open.2 fun U hU ⟨g, hg⟩ ↦ ?_⟩⟩

444 rcases isOpen_pi_iff.1 hU g hg with ⟨I, u, huo, huU⟩

445 have : ∀ i : I, ∃ y ∈ t i, y ∈ u i := fun i ↦

446 (htd i).exists_mem_open (huo i i.2).1 ⟨_, (huo i i.2).2⟩

447 choose y hyt hyu using this

448 lift y to ∀ i : I, t i using hyt

449 refine ⟨f ⟨I, y⟩, huU fun i (hi : i ∈ I) ↦ ?_, mem_range_self (f := f) ⟨I, y⟩⟩

450 simp only [f, dite_eq_left hi]

451 exact hyu ⟨i, _⟩

452

453instance [SeparableSpace α] {r : α → α → Prop} : SeparableSpace (Quot r) :=

454 isQuotientMap_quot_mk.separableSpace

455

456instance [SeparableSpace α] {s : Setoid α} : SeparableSpace (Quotient s) :=

457 isQuotientMap_quot_mk.separableSpace

458

459instance [TopologicalSpace β] [SeparableSpace α] [SeparableSpace β] : SeparableSpace (α ⊕ β) := by

460 obtain ⟨s, hsc, hsd⟩ := exists_countable_dense α

461 obtain ⟨t, htc, htd⟩ := exists_countable_dense β

462 refine ⟨Sum.inl '' s ∪ Sum.inr '' t, (hsc.image _).union (htc.image _), ?_⟩

463 simp_rw [dense_iff_closure_eq, closure_union, IsClosedEmbedding.inl.closure_image_eq,

464 hsd.closure_eq, IsClosedEmbedding.inr.closure_image_eq, htd.closure_eq, image_univ,

465 range_inl_union_range_inr]

466

467theorem separableSpace_sum_iff [TopologicalSpace β] :

468 SeparableSpace (α ⊕ β) ↔ SeparableSpace α ∧ SeparableSpace β :=

469 ⟨fun _ => ⟨(IsOpenEmbedding.inl (Y := β)).separableSpace,

470 (IsOpenEmbedding.inr (X := α)).separableSpace⟩, fun ⟨_, _⟩ => inferInstance⟩

471

472/-- A topological space with discrete topology is separable iff it is countable. -/

473theorem separableSpace_iff_countable [DiscreteTopology α] : SeparableSpace α ↔ Countable α := by

474 simp [separableSpace_iff, countable_univ_iff]

475

476/-- In a separable space, a family of nonempty disjoint open sets is countable. -/

477theorem _root_.Pairwise.countable_of_isOpen_disjoint [SeparableSpace α] {ι : Type*}

478 {s : ι → Set α} (hd : Pairwise (Disjoint on s)) (ho : ∀ i, IsOpen (s i))

479 (hne : ∀ i, (s i).Nonempty) : Countable ι := by

480 rcases exists_countable_dense α with ⟨u, u_countable, u_dense⟩

481 choose f hfu hfs using fun i ↦ u_dense.exists_mem_open (ho i) (hne i)

482 have f_inj : Injective f := fun i j hij ↦

483 hd.eq <| not_disjoint_iff.2 ⟨f i, hfs i, hij.symm ▸ hfs j⟩

484 have := u_countable.to_subtype

485 exact (f_inj.codRestrict hfu).countable

486

487/-- In a separable space, a family of nonempty disjoint open sets is countable. -/

488theorem _root_.Set.PairwiseDisjoint.countable_of_isOpen [SeparableSpace α] {ι : Type*}

489 {s : ι → Set α} {a : Set ι} (h : a.PairwiseDisjoint s) (ho : ∀ i ∈ a, IsOpen (s i))

490 (hne : ∀ i ∈ a, (s i).Nonempty) : a.Countable :=

491 (h.subtype _ _).countable_of_isOpen_disjoint (Subtype.forall.2 ho) (Subtype.forall.2 hne)

492

493/-- In a separable space, a family of disjoint sets with nonempty interiors is countable. -/

494theorem _root_.Set.PairwiseDisjoint.countable_of_nonempty_interior [SeparableSpace α] {ι : Type*}

495 {s : ι → Set α} {a : Set ι} (h : a.PairwiseDisjoint s)

496 (ha : ∀ i ∈ a, (interior (s i)).Nonempty) : a.Countable :=

497 (h.mono fun _ => interior_subset).countable_of_isOpen (fun _ _ => isOpen_interior) ha

498

499/-- A set `s` in a topological space is separable if it is contained in the closure of a countable

500set `c`. Beware that this definition does not require that `c` is contained in `s` (to express the

501latter, use `TopologicalSpace.SeparableSpace s` or

502`TopologicalSpace.IsSeparable (univ : Set s)`). In metric spaces, the two definitions are

503equivalent, see `TopologicalSpace.IsSeparable.separableSpace`. -/

504def IsSeparable (s : Set α) :=

505 ∃ c : Set α, c.Countable ∧ s ⊆ closure c

506

507theorem IsSeparable.mono {s u : Set α} (hs : IsSeparable s) (hu : u ⊆ s) : IsSeparable u := by

508 rcases hs with ⟨c, c_count, hs⟩

509 exact ⟨c, c_count, hu.trans hs⟩

510

511theorem IsSeparable.iUnion {ι : Sort*} [Countable ι] {s : ι → Set α}

512 (hs : ∀ i, IsSeparable (s i)) : IsSeparable (⋃ i, s i) := by

513 choose c hc h'c using hs

514 refine ⟨⋃ i, c i, countable_iUnion hc, iUnion_subset_iff.2 fun i => ?_⟩

515 exact (h'c i).trans (closure_mono (subset_iUnion _ i))

516

517@[simp]

518theorem isSeparable_iUnion {ι : Sort*} [Countable ι] {s : ι → Set α} :

519 IsSeparable (⋃ i, s i) ↔ ∀ i, IsSeparable (s i) :=

520 ⟨fun h i ↦ h.mono <| subset_iUnion s i, .iUnion⟩

521

522@[simp]

523theorem isSeparable_union {s t : Set α} : IsSeparable (s ∪ t) ↔ IsSeparable s ∧ IsSeparable t := by

524 simp [union_eq_iUnion, and_comm]

525

526theorem IsSeparable.union {s u : Set α} (hs : IsSeparable s) (hu : IsSeparable u) :

527 IsSeparable (s ∪ u) :=

528 isSeparable_union.2 ⟨hs, hu⟩

529

530@[simp]

531theorem isSeparable_closure : IsSeparable (closure s) ↔ IsSeparable s := by

532 simp only [IsSeparable, isClosed_closure.closure_subset_iff]

533

534protected alias ⟨_, IsSeparable.closure⟩ := isSeparable_closure

535

536theorem _root_.Set.Countable.isSeparable {s : Set α} (hs : s.Countable) : IsSeparable s :=

537 ⟨s, hs, subset_closure⟩

538

539theorem _root_.Set.Finite.isSeparable {s : Set α} (hs : s.Finite) : IsSeparable s :=

540 hs.countable.isSeparable

541

542theorem IsSeparable.univ_pi {ι : Type*} [Countable ι] {X : ι → Type*} {s : ∀ i, Set (X i)}

543 [∀ i, TopologicalSpace (X i)] (h : ∀ i, IsSeparable (s i)) :

544 IsSeparable (univ.pi s) := by

545 classical

546 rcases eq_empty_or_nonempty (univ.pi s) with he | ⟨f₀, -⟩

547 · rw [he]

548 exact countable_empty.isSeparable

549 · choose c c_count hc using h

550 have := fun i ↦ (c_count i).to_subtype

551 set g : (I : Finset ι) × ((i : I) → c i) → (i : ι) → X i := fun ⟨I, f⟩ i ↦

552 if hi : i ∈ I then f ⟨i, hi⟩ else f₀ i

553 refine ⟨range g, countable_range g, fun f hf ↦ mem_closure_iff.2 fun o ho hfo ↦ ?_⟩

554 rcases isOpen_pi_iff.1 ho f hfo with ⟨I, u, huo, hI⟩

555 rsuffices ⟨f, hf⟩ : ∃ f : (i : I) → c i, g ⟨I, f⟩ ∈ Set.pi I u

556 · exact ⟨g ⟨I, f⟩, hI hf, mem_range_self (f := g) ⟨I, f⟩⟩

557 suffices H : ∀ i ∈ I, (u i ∩ c i).Nonempty by

558 choose f hfu hfc using H

559 refine ⟨fun i ↦ ⟨f i i.2, hfc i i.2⟩, fun i (hi : i ∈ I) ↦ ?_⟩

560 simpa only [g, dite_eq_left hi] using hfu i hi

561 intro i hi

562 exact mem_closure_iff.1 (hc i <| hf _ trivial) _ (huo i hi).1 (huo i hi).2

563

564lemma isSeparable_pi {ι : Type*} [Countable ι] {α : ι → Type*} {s : ∀ i, Set (α i)}

565 [∀ i, TopologicalSpace (α i)] (h : ∀ i, IsSeparable (s i)) :

566 IsSeparable {f : ∀ i, α i | ∀ i, f i ∈ s i} := by

567 simpa only [← mem_univ_pi] using! IsSeparable.univ_pi h

568

569lemma IsSeparable.prod {β : Type*} [TopologicalSpace β]

570 {s : Set α} {t : Set β} (hs : IsSeparable s) (ht : IsSeparable t) :

571 IsSeparable (s ×ˢ t) := by

572 rcases hs with ⟨cs, cs_count, hcs⟩

573 rcases ht with ⟨ct, ct_count, hct⟩

574 refine ⟨cs ×ˢ ct, cs_count.prod ct_count, ?_⟩

575 rw [closure_prod_eq]

576 gcongr

577

578theorem IsSeparable.image {β : Type*} [TopologicalSpace β] {s : Set α} (hs : IsSeparable s)

579 {f : α → β} (hf : Continuous f) : IsSeparable (f '' s) := by

580 rcases hs with ⟨c, c_count, hc⟩

581 refine ⟨f '' c, c_count.image _, ?_⟩

582 rw [image_subset_iff]

583 exact hc.trans (closure_subset_preimage_closure_image hf)

584

585theorem _root_.Dense.isSeparable_iff (hs : Dense s) :

586 IsSeparable s ↔ SeparableSpace α := by

587 simp_rw [IsSeparable, separableSpace_iff, dense_iff_closure_eq, ← univ_subset_iff,

588 ← hs.closure_eq, isClosed_closure.closure_subset_iff]

589

590theorem isSeparable_univ_iff : IsSeparable (univ : Set α) ↔ SeparableSpace α :=

591 dense_univ.isSeparable_iff

592

593theorem isSeparable_range [TopologicalSpace β] [SeparableSpace α] {f : α → β} (hf : Continuous f) :

594 IsSeparable (range f) :=

595 image_univ (f := f) ▸ (isSeparable_univ_iff.2 ‹_›).image hf

596

597theorem IsSeparable.of_subtype (s : Set α) [SeparableSpace s] : IsSeparable s := by

598 simpa using isSeparable_range (continuous_subtype_val (p := (· ∈ s)))

599

600theorem IsSeparable.of_separableSpace [h : SeparableSpace α] (s : Set α) : IsSeparable s :=

601 IsSeparable.mono (isSeparable_univ_iff.2 h) (subset_univ _)

602

603end TopologicalSpace

604

605open TopologicalSpace

606

607protected theorem IsTopologicalBasis.iInf {β : Type*} {ι : Type*} {t : ι → TopologicalSpace β}

608 {T : ι → Set (Set β)} (h_basis : ∀ i, IsTopologicalBasis (t := t i) (T i)) :

609 IsTopologicalBasis (t := ⨅ i, t i)

610 { S | ∃ (U : ι → Set β) (F : Finset ι), (∀ i, i ∈ F → U i ∈ T i) ∧ S = ⋂ i ∈ F, U i } := by

611 let _ := ⨅ i, t i

612 refine isTopologicalBasis_of_isOpen_of_nhds ?_ ?_

613 · rintro - ⟨U, F, hU, rfl⟩

614 refine isOpen_biInter_finset fun i hi ↦

615 (h_basis i).isOpen (t := t i) (hU i hi) |>.mono (iInf_le _ _)

616 · intro a u ha hu

617 rcases (nhds_iInf (t := t) (a := a)).symm ▸ HasBasis.iInf'

618 (fun i ↦ (h_basis i).nhds_hasBasis (t := t i)) |>.mem_iff.1 (hu.mem_nhds ha)

619 with ⟨⟨F, U⟩, ⟨hF, hU⟩, hUu⟩

620 refine ⟨_, ⟨U, hF.toFinset, ?_, rfl⟩, ?_, ?_⟩ <;> simp only [Finite.mem_toFinset, mem_iInter]

621 · exact fun i hi ↦ (hU i hi).1

622 · exact fun i hi ↦ (hU i hi).2

623 · exact hUu

624

625theorem IsTopologicalBasis.iInf_induced {β : Type*} {ι : Type*} {X : ι → Type*}

626 [t : Π i, TopologicalSpace (X i)] {T : Π i, Set (Set (X i))}

627 (cond : ∀ i, IsTopologicalBasis (T i)) (f : Π i, β → X i) :

628 IsTopologicalBasis (t := ⨅ i, induced (f i) (t i))

629 { S | ∃ (U : ∀ i, Set (X i)) (F : Finset ι),

630 (∀ i, i ∈ F → U i ∈ T i) ∧ S = ⋂ (i) (_ : i ∈ F), f i ⁻¹' U i } := by

631 convert! IsTopologicalBasis.iInf (fun i ↦ (cond i).induced (f i)) with S

632 constructor <;> rintro ⟨U, F, hUT, hSU⟩

633 · exact ⟨fun i ↦ (f i) ⁻¹' (U i), F, fun i hi ↦ mem_image_of_mem _ (hUT i hi), hSU⟩

634 · choose! U' hU' hUU' using hUT

635 exact ⟨U', F, hU', hSU ▸ (.symm <| iInter₂_congr hUU')⟩

636

637theorem isTopologicalBasis_pi {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)]

638 {T : ∀ i, Set (Set (X i))} (cond : ∀ i, IsTopologicalBasis (T i)) :

639 IsTopologicalBasis { S | ∃ (U : ∀ i, Set (X i)) (F : Finset ι),

640 (∀ i, i ∈ F → U i ∈ T i) ∧ S = (F : Set ι).pi U } := by

641 simpa only [Set.pi_def] using! IsTopologicalBasis.iInf_induced cond eval

642

643theorem isTopologicalBasis_singletons (α : Type*) [TopologicalSpace α] [DiscreteTopology α] :

644 IsTopologicalBasis { s | ∃ x : α, (s : Set α) = {x} } :=

645 isTopologicalBasis_of_isOpen_of_nhds (fun _ _ => isOpen_discrete _) fun x _ hx _ =>

646 ⟨{x}, ⟨x, rfl⟩, mem_singleton x, singleton_subset_iff.2 hx⟩

647

648theorem isTopologicalBasis_subtype

649 {α : Type*} [TopologicalSpace α] {B : Set (Set α)}

650 (h : TopologicalSpace.IsTopologicalBasis B) (p : α → Prop) :

651 IsTopologicalBasis (Set.preimage (Subtype.val (p := p)) '' B) :=

652 IsInducing.subtypeVal.isTopologicalBasis h

653

654section

655variable {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)]

656

657lemma isOpenMap_eval (i : ι) : IsOpenMap (Function.eval i : (∀ i, X i) → X i) := by

658 classical

659 refine (isTopologicalBasis_pi fun _ ↦ isTopologicalBasis_opens).isOpenMap_iff.2 ?_

660 rintro _ ⟨U, s, hU, rfl⟩

661 obtain h | h := ((s : Set ι).pi U).eq_empty_or_nonempty

662 · simp [h]

663 by_cases hi : i ∈ s

664 · rw [eval_image_pi (mod_cast hi) h]

665 exact hU _ hi

666 · rw [eval_image_pi_of_notMem (mod_cast hi), ite_eq_left h]

667 exact isOpen_univ

668

669end

670

671theorem Dense.exists_countable_dense_subset {α : Type*} [TopologicalSpace α] {s : Set α}

672 [SeparableSpace s] (hs : Dense s) : ∃ t ⊆ s, t.Countable ∧ Dense t :=

673 let ⟨t, htc, htd⟩ := exists_countable_dense s

674 ⟨(↑) '' t, Subtype.coe_image_subset s t, htc.image Subtype.val,

675 hs.denseRange_val.dense_image continuous_subtype_val htd⟩

676

677/-- Let `s` be a dense set in a topological space `α` with partial order structure. If `s` is a

678separable space (e.g., if `α` has a second countable topology), then there exists a countable

679dense subset `t ⊆ s` such that `t` contains bottom/top element of `α` when they exist and belong

680to `s`. For a dense subset containing neither bot nor top elements, see

681`Dense.exists_countable_dense_subset_no_bot_top`. -/

682theorem Dense.exists_countable_dense_subset_bot_top {α : Type*} [TopologicalSpace α]

683 [PartialOrder α] {s : Set α} [SeparableSpace s] (hs : Dense s) :

684 ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ x, IsBot x → x ∈ s → x ∈ t) ∧

685 ∀ x, IsTop x → x ∈ s → x ∈ t := by

686 rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩

687 refine ⟨(t ∪ ({ x | IsBot x } ∪ { x | IsTop x })) ∩ s, ?_, ?_, ?_, ?_, ?_⟩

688 exacts [inter_subset_right,

689 (htc.union ((countable_isBot α).union (countable_isTop α))).mono inter_subset_left,

690 htd.mono (subset_inter subset_union_left hts), fun x hx hxs => ⟨Or.inr <| Or.inl hx, hxs⟩,

691 fun x hx hxs => ⟨Or.inr <| Or.inr hx, hxs⟩]

692

693instance separableSpace_univ {α : Type*} [TopologicalSpace α] [SeparableSpace α] :

694 SeparableSpace (univ : Set α) :=

695 (Equiv.Set.univ α).symm.surjective.denseRange.separableSpace (continuous_id.subtype_mk _)

696

697/-- If `α` is a separable topological space with a partial order, then there exists a countable

698dense set `s : Set α` that contains those of both bottom and top elements of `α` that actually

699exist. For a dense set containing neither bot nor top elements, see

700`exists_countable_dense_no_bot_top`. -/

701theorem exists_countable_dense_bot_top (α : Type*) [TopologicalSpace α] [SeparableSpace α]

702 [PartialOrder α] :

703 ∃ s : Set α, s.Countable ∧ Dense s ∧ (∀ x, IsBot x → x ∈ s) ∧ ∀ x, IsTop x → x ∈ s := by

704 simpa using dense_univ.exists_countable_dense_subset_bot_top

705

706namespace TopologicalSpace

707

708universe u

709

710variable (α : Type u) [t : TopologicalSpace α]

711

712/-- A first-countable space is one in which every point has a

713 countable neighborhood basis. -/

714class _root_.FirstCountableTopology : Prop where

715 /-- The filter `𝓝 a` is countably generated for all points `a`. -/

716 nhds_generated_countable : ∀ a : α, (𝓝 a).IsCountablyGenerated

717

718attribute [instance] FirstCountableTopology.nhds_generated_countable

719

720/-- If `β` is a first-countable space, then its induced topology via `f` on `α` is also

721first-countable. -/

722theorem firstCountableTopology_induced (α β : Type*) [t : TopologicalSpace β]

723 [FirstCountableTopology β] (f : α → β) : @FirstCountableTopology α (t.induced f) :=

724 let _ := t.induced f

725 ⟨fun x ↦ nhds_induced f x ▸ inferInstance⟩

726

727variable {α}

728

729instance Subtype.firstCountableTopology (s : Set α) [FirstCountableTopology α] :

730 FirstCountableTopology s :=

731 firstCountableTopology_induced s α (↑)

732

733protected theorem _root_.Topology.IsInducing.firstCountableTopology {β : Type*}

734 [TopologicalSpace β] [FirstCountableTopology β] {f : α → β} (hf : IsInducing f) :

735 FirstCountableTopology α := by

736 rw [hf.1]

737 exact firstCountableTopology_induced α β f

738

739protected theorem _root_.Topology.IsEmbedding.firstCountableTopology {β : Type*}

740 [TopologicalSpace β] [FirstCountableTopology β] {f : α → β} (hf : IsEmbedding f) :

741 FirstCountableTopology α :=

742 hf.1.firstCountableTopology

743

744section FirstCountableTopology

745

746variable [FirstCountableTopology α] {x : α}

747

748/-- In a first-countable space, a cluster point `x` of a countably generated filter is the limit of

749some sequence. -/

750theorem _root_.ClusterPt.exists_seq_tendsto {f : Filter α} [IsCountablyGenerated f]

751 (hx : ClusterPt x f) :

752 ∃ ψ : ℕ → α, Tendsto ψ atTop (𝓝 x) ∧ Tendsto ψ atTop f := by

753 unfold ClusterPt at hx

754 obtain ⟨g, hg⟩ := Filter.exists_seq_tendsto (𝓝 x ⊓ f)

755 exact ⟨g, (tendsto_inf.1 hg).1, (tendsto_inf.1 hg).2⟩

756

757theorem _root_.MapClusterPt.exists_seq_tendsto {ι : Type*} {f : Filter ι} [IsCountablyGenerated f]

758 {x : α} {u : ι → α} (hx : MapClusterPt x f u) :

759 ∃ ψ : ℕ → ι, Tendsto (u ∘ ψ) atTop (𝓝 x) ∧ Tendsto ψ atTop f := by

760 grind [exists_seq_comp_tendsto hx]

761

762/-- In a first-countable space, a cluster point `x` of a sequence

763is the limit of some subsequence. -/

764theorem _root_.MapClusterPt.tendsto_subseq {u : ℕ → α} (hx : MapClusterPt x atTop u) :

765 ∃ ψ : ℕ → ℕ, StrictMono ψ ∧ Tendsto (u ∘ ψ) atTop (𝓝 x) :=

766 subseq_tendsto_of_neBot hx

767

768@[deprecated MapClusterPt.tendsto_subseq (since := "2026-03-29")]

769theorem FirstCountableTopology.tendsto_subseq {u : ℕ → α} {x : α}

770 (hx : MapClusterPt x atTop u) : ∃ ψ : ℕ → ℕ, StrictMono ψ ∧ Tendsto (u ∘ ψ) atTop (𝓝 x) :=

771 subseq_tendsto_of_neBot hx

772

773end FirstCountableTopology

774

775instance {β} [TopologicalSpace β] [FirstCountableTopology α] [FirstCountableTopology β] :

776 FirstCountableTopology (α × β) :=

777 ⟨fun ⟨x, y⟩ => by rw [nhds_prod_eq]; infer_instance⟩

778

779section Pi

780

781instance {ι : Type*} {X : ι → Type*} [Countable ι] [∀ i, TopologicalSpace (X i)]

782 [∀ i, FirstCountableTopology (X i)] : FirstCountableTopology (∀ i, X i) :=

783 ⟨fun f => by rw [nhds_pi]; infer_instance⟩

784

785end Pi

786

787instance isCountablyGenerated_nhdsWithin (x : α) [IsCountablyGenerated (𝓝 x)] (s : Set α) :

788 IsCountablyGenerated (𝓝[s] x) :=

789 Inf.isCountablyGenerated _ _

790

791variable (α) in

792/-- A second-countable space is one with a countable basis. -/

793class _root_.SecondCountableTopology : Prop where

794 /-- There exists a countable set of sets that generates the topology. -/

795 is_open_generated_countable : ∃ b : Set (Set α), b.Countable ∧ t = TopologicalSpace.generateFrom b

796

797protected theorem IsTopologicalBasis.secondCountableTopology {b : Set (Set α)}

798 (hb : IsTopologicalBasis b) (hc : b.Countable) : SecondCountableTopology α :=

799 ⟨⟨b, hc, hb.eq_generateFrom⟩⟩

800

801lemma SecondCountableTopology.mk' {α} {b : Set (Set α)} (hc : b.Countable) :

802 @SecondCountableTopology α (generateFrom b) :=

803 @SecondCountableTopology.mk α (generateFrom b) ⟨b, hc, rfl⟩

804

805instance _root_.Finite.toSecondCountableTopology [Finite α] : SecondCountableTopology α where

806 is_open_generated_countable :=

807 ⟨_, {U | IsOpen U}.to_countable, TopologicalSpace.isTopologicalBasis_opens.eq_generateFrom⟩

808

809variable (α)

810

811theorem exists_countable_basis [SecondCountableTopology α] :

812 ∃ b : Set (Set α), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b := by

813 obtain ⟨b, hb₁, hb₂⟩ := @SecondCountableTopology.is_open_generated_countable α _ _

814 refine ⟨_, ?_, notMem_sdiff_of_mem ?_, (isTopologicalBasis_of_subbasis hb₂).sdiff_empty⟩

815 exacts [((countable_ofPred_finite_subset hb₁).image _).mono sdiff_subset, rfl]

816

817theorem exists_seq_basis [SecondCountableTopology α] :

818 ∃ b : ℕ → Set α, IsTopologicalBasis (range b) := by

819 obtain ⟨t, ht⟩ := TopologicalSpace.exists_countable_basis α

820 by_cases! hn : t.Nonempty

821 · obtain ⟨b, rfl⟩ := ht.1.exists_eq_range hn

822 exact ⟨b, ht.2.2⟩

823 · exact ⟨fun n => ∅, by simp_all⟩

824

825/-- A countable topological basis of `α`. -/

826def countableBasis [SecondCountableTopology α] : Set (Set α) :=

827 (exists_countable_basis α).choose

828

829theorem countable_countableBasis [SecondCountableTopology α] : (countableBasis α).Countable :=

830 (exists_countable_basis α).choose_spec.1

831

832instance encodableCountableBasis [SecondCountableTopology α] : Encodable (countableBasis α) :=

833 (countable_countableBasis α).toEncodable

834

835theorem empty_notMem_countableBasis [SecondCountableTopology α] : ∅ ∉ countableBasis α :=

836 (exists_countable_basis α).choose_spec.2.1

837

838theorem isBasis_countableBasis [SecondCountableTopology α] :

839 IsTopologicalBasis (countableBasis α) :=

840 (exists_countable_basis α).choose_spec.2.2

841

842theorem eq_generateFrom_countableBasis [SecondCountableTopology α] :

843 ‹TopologicalSpace α› = generateFrom (countableBasis α) :=

844 (isBasis_countableBasis α).eq_generateFrom

845

846variable {α}

847

848theorem isOpen_of_mem_countableBasis [SecondCountableTopology α] {s : Set α}

849 (hs : s ∈ countableBasis α) : IsOpen s :=

850 (isBasis_countableBasis α).isOpen hs

851

852theorem nonempty_of_mem_countableBasis [SecondCountableTopology α] {s : Set α}

853 (hs : s ∈ countableBasis α) : s.Nonempty :=

854 nonempty_iff_ne_empty.2 <| ne_of_mem_of_not_mem hs <| empty_notMem_countableBasis α

855

856variable (α)

857

858-- see Note [lower instance priority]

859instance (priority := 100) SecondCountableTopology.to_firstCountableTopology

860 [SecondCountableTopology α] : FirstCountableTopology α :=

861 ⟨fun _ => HasCountableBasis.isCountablyGenerated <|

862 ⟨(isBasis_countableBasis α).nhds_hasBasis,

863 (countable_countableBasis α).mono inter_subset_left⟩⟩

864

865-- see Note [lower instance priority]

866instance (priority := 100) [Countable α] [FirstCountableTopology α] :

867 SecondCountableTopology α where

868 is_open_generated_countable := by

869 -- The countable union of the countable neighborhood bases at each point is a countable basis.

870 choose b hxb hbb using fun x : α => (nhds_basis_opens x).exists_antitone_subbasis

871 use range b.uncurry, countable_range b.uncurry

872 apply le_antisymm

873 · rw [le_generateFrom_iff_subset_isOpen]

874 rintro _ ⟨⟨x, n⟩, rfl⟩

875 exact (hxb x n).right

876 · rw [le_iff_nhds]

877 intro x

878 rw [(hbb x).ge_iff]

879 intro n _

880 refine @IsOpen.mem_nhds α (generateFrom (range b.uncurry)) x (b x n) ?_ (hxb x n).left

881 exact isOpen_generateFrom_of_mem ⟨⟨x, n⟩, rfl⟩

882

883/-- If `β` is a second-countable space, then its induced topology via

884`f` on `α` is also second-countable. -/

885theorem secondCountableTopology_induced (α β) [t : TopologicalSpace β] [SecondCountableTopology β]

886 (f : α → β) : @SecondCountableTopology α (t.induced f) := by

887 rcases @SecondCountableTopology.is_open_generated_countable β _ _ with ⟨b, hb, eq⟩

888 let := t.induced f

889 refine { is_open_generated_countable := ⟨preimage f '' b, hb.image _, ?_⟩ }

890 rw [eq, induced_generateFrom_eq]

891

892variable {α}

893

894instance Subtype.secondCountableTopology (s : Set α) [SecondCountableTopology α] :

895 SecondCountableTopology s :=

896 secondCountableTopology_induced s α (↑)

897

898lemma secondCountableTopology_iInf {α ι} [Countable ι] {t : ι → TopologicalSpace α}

899 (ht : ∀ i, @SecondCountableTopology α (t i)) : @SecondCountableTopology α (⨅ i, t i) := by

900 rw [funext fun i => @eq_generateFrom_countableBasis α (t i) (ht i), ← generateFrom_iUnion]

901 exact SecondCountableTopology.mk' <|

902 countable_iUnion fun i => @countable_countableBasis _ (t i) (ht i)

903

904-- TODO: more fine grained instances for `FirstCountableTopology`, `SeparableSpace`, `T2Space`, ...

905instance {β : Type*} [TopologicalSpace β] [SecondCountableTopology α] [SecondCountableTopology β] :

906 SecondCountableTopology (α × β) :=

907 ((isBasis_countableBasis α).prod (isBasis_countableBasis β)).secondCountableTopology <|

908 (countable_countableBasis α).image2 (countable_countableBasis β) _

909

910instance {ι : Type*} {X : ι → Type*} [Countable ι] [∀ a, TopologicalSpace (X a)]

911 [∀ a, SecondCountableTopology (X a)] : SecondCountableTopology (∀ a, X a) :=

912 secondCountableTopology_iInf fun _ => secondCountableTopology_induced _ _ _

913

914-- see Note [lower instance priority]

915instance (priority := 100) SecondCountableTopology.to_separableSpace [SecondCountableTopology α] :

916 SeparableSpace α := by

917 choose p hp using fun s : countableBasis α => nonempty_of_mem_countableBasis s.2

918 exact ⟨⟨range p, countable_range _, (isBasis_countableBasis α).dense_iff.2 fun o ho _ =>

919 ⟨p ⟨o, ho⟩, hp ⟨o, _⟩, mem_range_self _⟩⟩⟩

920

921/-- A countable open cover induces a second-countable topology if all open covers

922are themselves second countable. -/

923theorem secondCountableTopology_of_countable_cover {ι} [Countable ι] {U : ι → Set α}

924 [∀ i, SecondCountableTopology (U i)] (Uo : ∀ i, IsOpen (U i)) (hc : ⋃ i, U i = univ) :

925 SecondCountableTopology α :=

926 haveI : IsTopologicalBasis (⋃ i, image ((↑) : U i → α) '' countableBasis (U i)) :=

927 isTopologicalBasis_of_cover Uo hc fun i => isBasis_countableBasis (U i)

928 this.secondCountableTopology (countable_iUnion fun _ => (countable_countableBasis _).image _)

929

930/-- In a second-countable space, an open set, given as a union of open sets,

931is equal to the union of countably many of those sets.

932In particular, any open covering of `α` has a countable subcover: α is a Lindelöf space. -/

933theorem isOpen_iUnion_countable [SecondCountableTopology α] {ι} (s : ι → Set α)

934 (H : ∀ i, IsOpen (s i)) : ∃ T : Set ι, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i := by

935 let B := { b ∈ countableBasis α | ∃ i, b ⊆ s i }

936 choose f hf using fun b : B => b.2.2

937 have : Countable B := ((countable_countableBasis α).mono (sep_subset _ _)).to_subtype

938 refine ⟨_, countable_range f, (iUnion₂_subset_iUnion _ _).antisymm (sUnion_subset ?_)⟩

939 rintro _ ⟨i, rfl⟩ x xs

940 rcases (isBasis_countableBasis α).exists_subset_of_mem_open xs (H _) with ⟨b, hb, xb, bs⟩

941 exact ⟨_, ⟨_, rfl⟩, _, ⟨⟨⟨_, hb, _, bs⟩, rfl⟩, rfl⟩, hf _ xb⟩

942

943theorem isOpen_biUnion_countable [SecondCountableTopology α] {ι : Type*} (I : Set ι) (s : ι → Set α)

944 (H : ∀ i ∈ I, IsOpen (s i)) : ∃ T ⊆ I, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i ∈ I, s i := by

945 simp_rw [← Subtype.exists_set_subtype, biUnion_image]

946 rcases isOpen_iUnion_countable (fun i : I ↦ s i) fun i ↦ H i i.2 with ⟨T, hTc, hU⟩

947 exact ⟨T, hTc.image _, hU.trans <| iUnion_subtype ..⟩

948

949theorem isOpen_sUnion_countable [SecondCountableTopology α] (S : Set (Set α))

950 (H : ∀ s ∈ S, IsOpen s) : ∃ T : Set (Set α), T.Countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S := by

951 simpa only [and_left_comm, sUnion_eq_biUnion] using! isOpen_biUnion_countable S id H

952

953/-- In a topological space with second countable topology, if `f` is a function that sends each

954point `x` to a neighborhood of `x`, then for some countable set `s`, the neighborhoods `f x`,

955`x ∈ s`, cover the whole space. -/

956theorem countable_cover_nhds [SecondCountableTopology α] {f : α → Set α} (hf : ∀ x, f x ∈ 𝓝 x) :

957 ∃ s : Set α, s.Countable ∧ ⋃ x ∈ s, f x = univ := by

958 rcases isOpen_iUnion_countable (fun x => interior (f x)) fun x => isOpen_interior with

959 ⟨s, hsc, hsU⟩

960 suffices ⋃ x ∈ s, interior (f x) = univ from

961 ⟨s, hsc, flip eq_univ_of_subset this <| iUnion₂_mono fun _ _ => interior_subset⟩

962 simp only [hsU, eq_univ_iff_forall, mem_iUnion]

963 exact fun x => ⟨x, mem_interior_iff_mem_nhds.2 (hf x)⟩

964

965theorem countable_cover_nhdsWithin [SecondCountableTopology α] {f : α → Set α} {s : Set α}

966 (hf : ∀ x ∈ s, f x ∈ 𝓝[s] x) : ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x := by

967 have : ∀ x : s, (↑) ⁻¹' f x ∈ 𝓝 x := fun x => preimage_coe_mem_nhds_subtype.2 (hf x x.2)

968 rcases countable_cover_nhds this with ⟨t, htc, htU⟩

969 refine ⟨(↑) '' t, Subtype.coe_image_subset _ _, htc.image _, fun x hx => ?_⟩

970 simp only [biUnion_image, eq_univ_iff_forall, ← preimage_iUnion, mem_preimage] at htU ⊢

971 exact htU ⟨x, hx⟩

972

973/-- In a second countable topological space, any open set is a countable union of elements in a

974given topological basis. -/

975lemma IsTopologicalBasis.exists_countable_biUnion_of_isOpen [SecondCountableTopology α]

976 {t : Set (Set α)} (ht : IsTopologicalBasis t) {u : Set α} (hu : IsOpen u) :

977 ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a := by

978 have A : ∀ x ∈ u, ∃ a ∈ t, x ∈ a ∧ a ⊆ u :=

979 fun x hx ↦ ht.exists_subset_of_mem_open hx hu

980 choose! a hat xa au using A

981 obtain ⟨T, T_count, hT⟩ : ∃ T : Set u, T.Countable ∧ ⋃ i ∈ T, a i = ⋃ (i : u), a i := by

982 apply isOpen_iUnion_countable _

983 rintro ⟨x, hx⟩

984 exact ht.isOpen (hat x hx)

985 refine ⟨(fun (x : u) ↦ a x) '' T, ?_, T_count.image _, ?_⟩

986 · simp only [image_subset_iff]

987 rintro ⟨x, xu⟩ -

988 exact hat x xu

989 rw [biUnion_image, hT]

990 apply Subset.antisymm

991 · intro x hx

992 simp

993 grind

994 · simp

995 grind

996

997/-- In a second countable topological space, any topological basis contains a countable subset

998which is also a topological basis. -/

999lemma IsTopologicalBasis.exists_countable

1000 [SecondCountableTopology α] {t : Set (Set α)} (ht : IsTopologicalBasis t) :

1001 ∃ s ⊆ t, s.Countable ∧ IsTopologicalBasis s := by

1002 have A : ∀ u ∈ countableBasis α, ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a :=

1003 fun u hu ↦ ht.exists_countable_biUnion_of_isOpen ((isBasis_countableBasis α).isOpen hu)

1004 choose! s hst s_count hs using A

1005 refine ⟨⋃ u ∈ countableBasis α, s u, by simpa using hst,

1006 (countable_countableBasis α).biUnion s_count, ?_⟩

1007 apply isTopologicalBasis_of_isOpen_of_nhds

1008 · simp only [mem_iUnion, exists_prop, forall_exists_index, and_imp]

1009 have := @ht.isOpen

1010 grind

1011 · intro x v hx hv

1012 simp only [mem_iUnion, exists_prop]

1013 obtain ⟨u, u_mem, xu, uv⟩ : ∃ u ∈ countableBasis α, x ∈ u ∧ u ⊆ v :=

1014 (isBasis_countableBasis α).isOpen_iff.1 hv _ hx

1015 have : x ∈ ⋃ a ∈ s u, a := by

1016 convert! xu

1017 exact (hs u u_mem).symm

1018 obtain ⟨w, ws, xw⟩ : ∃ w ∈ s u, x ∈ w := by simpa using this

1019 refine ⟨w, ⟨u, u_mem, ws⟩, xw, ?_⟩

1020 apply Subset.trans (Subset.trans _ (hs u u_mem).symm.subset) uv

1021 exact subset_iUnion₂_of_subset w ws (Subset.refl _)

1022

1023/-- In a second countable topological space, any family generating the topology admits a

1024countable generating subfamily. -/

1025lemma exists_countable_of_generateFrom

1026 {α : Type*} [ts : TopologicalSpace α] [SecondCountableTopology α] {t : Set (Set α)}

1027 (ht : ts = generateFrom t) :

1028 ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s := by

1029 let t' := (fun f => ⋂₀ f) '' { f : Set (Set α) | f.Finite ∧ f ⊆ t }

1030 have : IsTopologicalBasis t' := TopologicalSpace.isTopologicalBasis_of_subbasis ht

1031 obtain ⟨s', s't', s'_count, hs'⟩ : ∃ s' ⊆ t', s'.Countable ∧ IsTopologicalBasis s' :=

1032 this.exists_countable

1033 have A : ∀ u ∈ s', ∃ (f : Set (Set α)), f.Finite ∧ f ⊆ t ∧ ⋂₀ f = u :=

1034 fun u hu ↦ by simpa [t', and_assoc] using s't' hu

1035 choose! f f_fin ft hf using A

1036 refine ⟨⋃ u ∈ s', f u, by simpa using ft, ?_, ?_⟩

1037 · apply s'_count.biUnion

1038 intro u hu

1039 exact Finite.countable (f_fin u hu)

1040 · apply le_antisymm

1041 · apply le_generateFrom_iff_subset_isOpen.2

1042 simp only [iUnion_subset_iff]

1043 intro u hu v hv

1044 rw [ht]

1045 apply isOpen_generateFrom_of_mem

1046 exact ft u hu hv

1047 · rw [hs'.eq_generateFrom]

1048 apply le_generateFrom_iff_subset_isOpen.2

1049 intro u hu

1050 rw [← hf u hu, sInter_eq_biInter]

1051 change IsOpen[generateFrom _] (⋂ i ∈ f u, i)

1052 apply @Finite.isOpen_biInter _ _ (generateFrom (⋃ u ∈ s', f u)) _ _

1053 · apply f_fin u hu

1054 · intro i hi

1055 apply isOpen_generateFrom_of_mem

1056 simp

1057 grind

1058

1059section Sigma

1060

1061variable {ι : Type*} {E : ι → Type*} [∀ i, TopologicalSpace (E i)]

1062

1063/-- In a disjoint union space `Σ i, E i`, one can form a topological basis by taking the union of

1064topological bases on each of the parts of the space. -/

1065theorem IsTopologicalBasis.sigma {s : ∀ i : ι, Set (Set (E i))}

1066 (hs : ∀ i, IsTopologicalBasis (s i)) :

1067 IsTopologicalBasis (⋃ i : ι, (fun u => (Sigma.mk i '' u : Set (Σ i, E i))) '' s i) := by

1068 refine .of_hasBasis_nhds fun a ↦ ?_

1069 rw [Sigma.nhds_eq]

1070 convert! (((hs a.1).nhds_hasBasis).map _).to_image_id

1071 aesop

1072

1073/-- A countable disjoint union of second countable spaces is second countable. -/

1074instance [Countable ι] [∀ i, SecondCountableTopology (E i)] :

1075 SecondCountableTopology (Σ i, E i) := by

1076 let b := ⋃ i : ι, (fun u => (Sigma.mk i '' u : Set (Σ i, E i))) '' countableBasis (E i)

1077 have A : IsTopologicalBasis b := IsTopologicalBasis.sigma fun i => isBasis_countableBasis _

1078 have B : b.Countable := countable_iUnion fun i => (countable_countableBasis _).image _

1079 exact A.secondCountableTopology B

1080

1081end Sigma

1082

1083section Sum

1084

1085variable {β : Type*} [TopologicalSpace β]

1086

1087/-- In a sum space `α ⊕ β`, one can form a topological basis by taking the union of

1088topological bases on each of the two components. -/

1089theorem IsTopologicalBasis.sum {s : Set (Set α)} (hs : IsTopologicalBasis s) {t : Set (Set β)}

1090 (ht : IsTopologicalBasis t) :

1091 IsTopologicalBasis ((fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t) := by

1092 apply isTopologicalBasis_of_isOpen_of_nhds

1093 · rintro u (⟨w, hw, rfl⟩ | ⟨w, hw, rfl⟩)

1094 · exact IsOpenEmbedding.inl.isOpenMap w (hs.isOpen hw)

1095 · exact IsOpenEmbedding.inr.isOpenMap w (ht.isOpen hw)

1096 · rintro (x | x) u hxu u_open

1097 · obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ s, x ∈ v ∧ v ⊆ Sum.inl ⁻¹' u :=

1098 hs.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).1

1099 exact ⟨Sum.inl '' v, mem_union_left _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,

1100 image_subset_iff.2 vu⟩

1101 · obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ t, x ∈ v ∧ v ⊆ Sum.inr ⁻¹' u :=

1102 ht.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).2

1103 exact ⟨Sum.inr '' v, mem_union_right _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,

1104 image_subset_iff.2 vu⟩

1105

1106/-- A sum type of two second countable spaces is second countable. -/

1107instance [SecondCountableTopology α] [SecondCountableTopology β] :

1108 SecondCountableTopology (α ⊕ β) := by

1109 let b :=

1110 (fun u => Sum.inl '' u) '' countableBasis α ∪ (fun u => Sum.inr '' u) '' countableBasis β

1111 have A : IsTopologicalBasis b := (isBasis_countableBasis α).sum (isBasis_countableBasis β)

1112 have B : b.Countable :=

1113 (Countable.image (countable_countableBasis _) _).union

1114 (Countable.image (countable_countableBasis _) _)

1115 exact A.secondCountableTopology B

1116

1117end Sum

1118

1119section Quotient

1120

1121variable {X : Type*} [TopologicalSpace X] {Y : Type*} [TopologicalSpace Y] {π : X → Y}

1122

1123/-- The image of a topological basis under an open quotient map is a topological basis. -/

1124theorem _root_.IsOpenQuotientMap.isTopologicalBasis (h : IsOpenQuotientMap π)

1125 {V : Set (Set X)} (hV : IsTopologicalBasis V) : IsTopologicalBasis (Set.image π '' V) := by

1126 refine .of_hasBasis_nhds <| h.surjective.forall.mpr fun x ↦ ?_

1127 have : 𝓝 (π x) |>.HasBasis (fun s ↦ s ∈ V ∧ x ∈ s) (fun s ↦ π '' s) := by

1128 simpa only [← h.map_nhds_eq] using hV.nhds_hasBasis.map _

1129 refine this.to_hasBasis' ?_ ?_

1130 · intro s ⟨hs, hxs⟩

1131 exact ⟨π '' s, ⟨mem_image_of_mem _ hs, mem_image_of_mem _ hxs⟩, .rfl⟩

1132 · rintro - ⟨⟨s, hs, rfl⟩, hxs⟩

1133 exact h.isOpenMap s (hV.isOpen hs) |>.mem_nhds hxs

1134

1135@[deprecated IsOpenQuotientMap.isTopologicalBasis (since := "2026-08-21")]

1136theorem IsTopologicalBasis.isQuotientMap {V : Set (Set X)} (hV : IsTopologicalBasis V)

1137 (h' : IsQuotientMap π) (h : IsOpenMap π) : IsTopologicalBasis (Set.image π '' V) :=

1138 IsOpenQuotientMap.isTopologicalBasis (.of_isOpenMap_isQuotientMap h h') hV

1139

1140/-- A second countable space is mapped by an open quotient map to a second countable space. -/

1141theorem _root_.Topology.IsOpenQuotientMap.secondCountableTopology [SecondCountableTopology X]

1142 (h : IsOpenQuotientMap π) : SecondCountableTopology Y where

1143 is_open_generated_countable := by

1144 obtain ⟨V, V_countable, -, V_generates⟩ := exists_countable_basis X

1145 exact ⟨Set.image π '' V, V_countable.image (Set.image π),

1146 (h.isTopologicalBasis V_generates).eq_generateFrom⟩

1147

1148@[deprecated IsOpenQuotientMap.isTopologicalBasis (since := "2026-08-21")]

1149theorem _root_.Topology.IsQuotientMap.secondCountableTopology [SecondCountableTopology X]

1150 (h' : IsQuotientMap π) (h : IsOpenMap π) : SecondCountableTopology Y :=

1151 IsOpenQuotientMap.secondCountableTopology ⟨h'.surjective, h'.continuous, h⟩

1152

1153variable {S : Setoid X}

1154

1155/-- The image of a topological basis "downstairs" in an open quotient is a topological basis. -/

1156theorem IsTopologicalBasis.quotient {V : Set (Set X)} (hV : IsTopologicalBasis V)

1157 (h : IsOpenMap (Quotient.mk' : X → Quotient S)) :

1158 IsTopologicalBasis (Set.image (Quotient.mk' : X → Quotient S) '' V) :=

1159 IsOpenQuotientMap.of_isOpenMap_isQuotientMap h isQuotientMap_quotient_mk'

1160 |>.isTopologicalBasis hV

1161

1162/-- An open quotient of a second countable space is second countable. -/

1163theorem Quotient.secondCountableTopology [SecondCountableTopology X]

1164 (h : IsOpenMap (Quotient.mk' : X → Quotient S)) : SecondCountableTopology (Quotient S) :=

1165 IsOpenQuotientMap.of_isOpenMap_isQuotientMap h isQuotientMap_quotient_mk'

1166 |>.secondCountableTopology

1167

1168end Quotient

1169

1170end TopologicalSpace

1171

1172open TopologicalSpace

1173

1174variable {α β : Type*} [TopologicalSpace α] {f : α → β}

1175

1176protected theorem Topology.IsInducing.secondCountableTopology [TopologicalSpace β]

1177 [SecondCountableTopology β] (hf : IsInducing f) : SecondCountableTopology α := by

1178 rw [hf.1]

1179 exact secondCountableTopology_induced α β f

1180

1181protected theorem Topology.IsEmbedding.secondCountableTopology

1182 [TopologicalSpace β] [SecondCountableTopology β]

1183 (hf : IsEmbedding f) : SecondCountableTopology α :=

1184 hf.1.secondCountableTopology

1185

1186protected theorem Topology.IsEmbedding.separableSpace

1187 [TopologicalSpace β] [SecondCountableTopology β] {f : α → β} (hf : IsEmbedding f) :

1188 TopologicalSpace.SeparableSpace α := by

1189 have := hf.secondCountableTopology

1190 exact SecondCountableTopology.to_separableSpace