biInter_biUnion_ball — Mathlib

English

If p indexes a basis of the uniformity with sets U, then for any finite set s, the intersection over i of the unions of balls ball x U i equals the closure of s.

Русский

Пусть p индексирует базис равномерности через множества U, тогда пересечение по i всех объединений шаров ball x (U i) по x∈s даёт замыкание s.

LaTeX

$$$ \bigcap_i (\,\forall _ : p i, \; \bigcup_{x \in s} \mathrm{ball}\, x (U i) \,) = \overline{s} $$$

Lean4

theorem biInter_biUnion_ball {p : ι → Prop} {U : ι → Set (α × α)} (h : HasBasis (𝓤 α) p U) (s : Set α) :
    (⋂ (i) (_ : p i), ⋃ x ∈ s, ball x (U i)) = closure s :=
  by
  ext x
  simp [mem_closure_iff_nhds_basis (nhds_basis_uniformity h), ball]

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