English
A separable uniform space with a countably generated uniformity filter is second countable.
Русский
Разделимое равномерное пространство с счетной базой фильтра равномерности — второе счетное топологическое основание.
LaTeX
$$$[\text{SeparableSpace}(\alpha)] \Rightarrow \text{SecondCountableTopology}(\alpha)$$$
Lean4
/-- A separable uniform space with countably generated uniformity filter is second countable:
one obtains a countable basis by taking the balls centered at points in a dense subset,
and with rational "radii" from a countable open symmetric antitone basis of `𝓤 α`. -/
instance secondCountable_of_separable [SeparableSpace α] : SecondCountableTopology α :=
by
rcases exists_countable_dense α with ⟨s, hsc, hsd⟩
obtain
⟨t : ℕ → Set (α × α), hto : ∀ i : ℕ, t i ∈ (𝓤 α).sets ∧ IsOpen (t i) ∧ IsSymmetricRel (t i), h_basis :
(𝓤 α).HasAntitoneBasis t⟩ :=
(@uniformity_hasBasis_open_symmetric α _).exists_antitone_subbasis
choose ht_mem hto hts using hto
refine ⟨⟨⋃ x ∈ s, range fun k => ball x (t k), hsc.biUnion fun x _ => countable_range _, ?_⟩⟩
refine (isTopologicalBasis_of_isOpen_of_nhds ?_ ?_).eq_generateFrom
· simp only [mem_iUnion₂, mem_range]
rintro _ ⟨x, _, k, rfl⟩
exact isOpen_ball x (hto k)
· intro x V hxV hVo
simp only [mem_iUnion₂, mem_range, exists_prop]
rcases UniformSpace.mem_nhds_iff.1 (IsOpen.mem_nhds hVo hxV) with ⟨U, hU, hUV⟩
rcases comp_symm_of_uniformity hU with ⟨U', hU', _, hUU'⟩
rcases h_basis.toHasBasis.mem_iff.1 hU' with ⟨k, -, hk⟩
rcases
hsd.inter_open_nonempty (ball x <| t k) (isOpen_ball x (hto k)) ⟨x, UniformSpace.mem_ball_self _ (ht_mem k)⟩ with
⟨y, hxy, hys⟩
refine ⟨_, ⟨y, hys, k, rfl⟩, (hts k).subset hxy, fun z hz => ?_⟩
exact hUV (ball_subset_of_comp_subset (hk hxy) hUU' (hk hz))
