English
A pseudometric space is second countable if for every ε>0 there exists a countable ε-dense set.
Русский
Псевдометрическое пространство второй счетности, если для каждого ε>0 существует счетное ε-плотное множество.
LaTeX
$$$\\forall \\varepsilon>0, \\exists s \\subseteq \\alpha:\\ s\\text{Countable} \\land \\forall x, \\exists y\\in s, \\operatorname{dist}(x,y) \\le \\varepsilon$$$
Lean4
/-- A pseudometric space is second countable if, for every `ε > 0`, there is a countable set which
is `ε`-dense. -/
theorem secondCountable_of_almost_dense_set (H : ∀ ε > (0 : ℝ), ∃ s : Set α, s.Countable ∧ ∀ x, ∃ y ∈ s, dist x y ≤ ε) :
SecondCountableTopology α :=
by
refine EMetric.secondCountable_of_almost_dense_set fun ε ε0 => ?_
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 ε0 with ⟨ε', ε'0, ε'ε⟩
choose s hsc y hys hyx using H ε' (mod_cast ε'0)
refine ⟨s, hsc, iUnion₂_eq_univ_iff.2 fun x => ⟨y x, hys _, le_trans ?_ ε'ε.le⟩⟩
exact mod_cast hyx x
