closure_eq_inter_uniformity — Mathlib

English

If 𝓤 α has a basis with index p and sets U, then (𝓤 α) has a basis with the sets closure(U i).

Русский

Если у 𝓤 α есть базис с индексами p и наборами U, то (𝓤 α) имеет базис с множествами closure(U_i).

LaTeX

$$$(𝓤 α).HasBasis p U \Rightarrow (𝓤 α).HasBasis p (\\lambda i, closure (U i))$$$

Lean4

theorem closure_eq_inter_uniformity {t : Set (α × α)} : closure t = ⋂ d ∈ 𝓤 α, d ○ (t ○ d) :=
  calc
    closure t = ⋂ (V) (_ : V ∈ 𝓤 α ∧ IsSymmetricRel V), V ○ t ○ V := closure_eq_uniformity t
    _ = ⋂ V ∈ 𝓤 α, V ○ t ○ V :=
      (Eq.symm <|
        UniformSpace.hasBasis_symmetric.biInter_mem fun _ _ hV => compRel_mono (compRel_mono hV Subset.rfl) hV)
    _ = ⋂ V ∈ 𝓤 α, V ○ (t ○ V) := by simp only [compRel_assoc]

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