English
The same as above for a dense range xs: if xs: ι → α is dense and U ∈ 𝓤 α, then ⋃ i UniformSpace.ball(xs(i), U) = univ.
Русский
То же самое в случае плотной диапазонной функции xs: если xs: ι → α плотная, и U ∈ 𝓤 α, то ⋃ i UniformSpace.ball(xs(i), U) = univ.
LaTeX
$$$\bigcup_{i} \mathrm{ball}(xs(i), U) = \mathsf{univ}$$$
Lean4
/-- The uniform neighborhoods of all points of a dense indexed collection cover the whole space. -/
theorem iUnion_uniformity_ball {ι : Type*} {xs : ι → α} (xs_dense : DenseRange xs) {U : Set (α × α)}
(hU : U ∈ uniformity α) : ⋃ i, UniformSpace.ball (xs i) U = univ :=
by
rw [← biUnion_range (f := xs) (g := fun x ↦ UniformSpace.ball x U)]
exact Dense.biUnion_uniformity_ball xs_dense hU