English
Let α be a uniform space. The entourages 𝓤(α) form a filter on α×α. This filter has a basis consisting of closed sets: there exists a collection of closed entourages {V} ⊆ 𝓤(α) such that every entourage E ∈ 𝓤(α) contains some closed V with V ⊆ E.
Русский
Пусть α — униформное пространство. Множество энтурджей 𝓤(α) образует фильтр на α×α. Этот фильтр имеет базис, состоящий из замкнутых множеств: существуетfamily замкнутых энтурджей {V} ⊆ 𝓤(α), такой что для любого энтурджа E ∈ 𝓤(α) существует замкнутая V с V ⊆ E.
LaTeX
$$$\\HasBasis (\\mathcal{U} α) (\\lambda V : \\mathrm{Set}(α \\times α) \\,=> \\ V \\in \\mathcal{U} α \\land \\mathrm{IsClosed} V) \\mathrm{id}$$$
Lean4
theorem uniformity_hasBasis_closed : HasBasis (𝓤 α) (fun V : Set (α × α) => V ∈ 𝓤 α ∧ IsClosed V) id :=
by
refine Filter.hasBasis_self.2 fun t h => ?_
rcases comp_comp_symm_mem_uniformity_sets h with ⟨w, w_in, w_symm, r⟩
refine ⟨closure w, mem_of_superset w_in subset_closure, isClosed_closure, ?_⟩
refine Subset.trans ?_ r
rw [closure_eq_uniformity]
apply iInter_subset_of_subset
apply iInter_subset
exact ⟨w_in, w_symm⟩
