iUnion_uniformity_ball — Mathlib

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

Похожие утверждения