uniformity_closure — Mathlib

English

If the uniformity has a basis given by sets U_i with index i, then the closures of those sets form a basis for the same uniformity: (𝓤 α).HasBasis p U ⇒ (𝓤 α).HasBasis p (λ i, closure (U i)).

Русский

Если у униформности есть базис, заданный наборами U_i с индексами i, то замыкания этих множест́в образуют базис той же униформности: (𝓤 α).HasBasis p U ⇒ (𝓤 α).HasBasis p (λ i, closure (U i)).

LaTeX

$$$(𝓤 α).HasBasis p U \Rightarrow (𝓤 α).HasBasis p (\\lambda i, \\overline{U(i)})$$$

Lean4

theorem uniformity_closure {p : ι → Prop} {U : ι → Set (α × α)} (h : (𝓤 α).HasBasis p U) :
    (𝓤 α).HasBasis p fun i => closure (U i) :=
  (@uniformity_eq_uniformity_closure α _).symm ▸ h.lift'_closure

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