English
If a set s is separable, then there exists a countable dense subset t ⊆ s such that s ⊆ closure t.
Русский
Если множество s разделимо, то существует счетное плотное подмножество t ⊆ s такое, что s ⊆ closure t.
LaTeX
$$∃ t, t ⊆ s ∧ t.Countable ∧ s ⊆ closure t$$
Lean4
/-- If a set `s` is separable in a (pseudo extended) metric space, then it admits a countable dense
subset. This is not obvious, as the countable set whose closure covers `s` given by the definition
of separability does not need in general to be contained in `s`. -/
theorem exists_countable_dense_subset {s : Set α} (hs : IsSeparable s) : ∃ t, t ⊆ s ∧ t.Countable ∧ s ⊆ closure t :=
by
have : ∀ ε > 0, ∃ t : Set α, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε := fun ε ε0 =>
by
rcases hs with ⟨t, htc, hst⟩
refine ⟨t, htc, hst.trans fun x hx => ?_⟩
rcases mem_closure_iff.1 hx ε ε0 with ⟨y, hyt, hxy⟩
exact mem_iUnion₂.2 ⟨y, hyt, mem_closedBall.2 hxy.le⟩
exact subset_countable_closure_of_almost_dense_set _ this
