English
If s is a set in a pseudo-emetric space such that for every ε > 0 there is a countable ε-dense approximation in s, then there exists a countable t ⊆ s with s ⊆ closure(t).
Русский
Если s — множество в псевдоэметрическом пространстве, и для каждого ε > 0 существует счётное множество t,ε⊆s, которое ε-плотно приближает s, то существует счётное подмножество t ⊆ s такое, что s ⊆ closure(t).
LaTeX
$$$\\exists t\\subseteq s,\\; t \\text{ счётно},\\; s \\subseteq \\overline{t}$$$
Lean4
/-- For a set `s` in a pseudo emetric space, if for every `ε > 0` there exists a countable
set that is `ε`-dense in `s`, then there exists a countable subset `t ⊆ s` that is dense in `s`. -/
theorem subset_countable_closure_of_almost_dense_set (s : Set α)
(hs : ∀ ε > 0, ∃ t : Set α, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε) : ∃ t, t ⊆ s ∧ t.Countable ∧ s ⊆ closure t :=
by
rcases s.eq_empty_or_nonempty with (rfl | ⟨x₀, hx₀⟩)
· exact ⟨∅, empty_subset _, countable_empty, empty_subset _⟩
choose! T hTc hsT using fun n : ℕ => hs n⁻¹ (by simp)
have : ∀ r x, ∃ y ∈ s, closedBall x r ∩ s ⊆ closedBall y (r * 2) := fun r x =>
by
rcases (closedBall x r ∩ s).eq_empty_or_nonempty with (he | ⟨y, hxy, hys⟩)
· refine ⟨x₀, hx₀, ?_⟩
rw [he]
exact empty_subset _
· refine ⟨y, hys, fun z hz => ?_⟩
calc
edist z y ≤ edist z x + edist y x := edist_triangle_right _ _ _
_ ≤ r + r := (add_le_add hz.1 hxy)
_ = r * 2 := (mul_two r).symm
choose f hfs hf using this
refine
⟨⋃ n : ℕ, f n⁻¹ '' T n, iUnion_subset fun n => image_subset_iff.2 fun z _ => hfs _ _,
countable_iUnion fun n => (hTc n).image _, ?_⟩
refine fun x hx => mem_closure_iff.2 fun ε ε0 => ?_
rcases ENNReal.exists_inv_nat_lt (ENNReal.half_pos ε0.lt.ne').ne' with ⟨n, hn⟩
rcases mem_iUnion₂.1 (hsT n hx) with ⟨y, hyn, hyx⟩
refine ⟨f n⁻¹ y, mem_iUnion.2 ⟨n, mem_image_of_mem _ hyn⟩, ?_⟩
calc
edist x (f n⁻¹ y) ≤ (n : ℝ≥0∞)⁻¹ * 2 := hf _ _ ⟨hyx, hx⟩
_ < ε := ENNReal.mul_lt_of_lt_div hn
