biUnion_uniformity_ball — Mathlib

English

If s is dense and U ∈ 𝓤 α, then the union over x∈s of ball(x,U) equals the whole space: ⋃ x∈s ball(x,U) = univ.

Русский

Если s плотно, и U ∈ 𝓤 α, то объединение всех шаров ball(x,U) по x∈s покрывает всю пространство.

LaTeX

$$$⋃_{x∈s} \mathrm{ball}(x,U) = \mathsf{univ}$$$

Lean4

/-- The uniform neighborhoods of all points of a dense set cover the whole space. -/
theorem biUnion_uniformity_ball {s : Set α} {U : Set (α × α)} (hs : Dense s) (hU : U ∈ 𝓤 α) :
    ⋃ x ∈ s, ball x U = univ := by
  refine iUnion₂_eq_univ_iff.2 fun y => ?_
  rcases hs.inter_nhds_nonempty (mem_nhds_right y hU) with ⟨x, hxs, hxy : (x, y) ∈ U⟩
  exact ⟨x, hxs, hxy⟩

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