English
The basis can be refined to symmetric open entourages: open, symmetric V with V○V ⊆ s for any s ∈ 𝓤 α.
Русский
Базис можно привести к открытым симметричным энтурджам: открытые, симметричные V такие, что V○V ⊆ s для любого s ∈ 𝓤 α.
LaTeX
$$$\text{HasBasis}(\mathcal{U} α)\bigl(\text{fun } V \Rightarrow V ∈ \mathcal{U} α ∧ \mathrm{IsOpen} V ∧ \mathrm{IsSymmetricRel} V\bigr) id$$$
Lean4
/-- Open elements `s : Set (α × α)` of `𝓤 α` such that `(x, y) ∈ s ↔ (y, x) ∈ s` form a basis
of `𝓤 α`. -/
theorem uniformity_hasBasis_open_symmetric :
HasBasis (𝓤 α) (fun V : Set (α × α) => V ∈ 𝓤 α ∧ IsOpen V ∧ IsSymmetricRel V) id :=
by
simp only [← and_assoc]
refine uniformity_hasBasis_open.restrict fun s hs => ⟨symmetrizeRel s, ?_⟩
exact
⟨⟨symmetrize_mem_uniformity hs.1, IsOpen.inter hs.2 (hs.2.preimage continuous_swap)⟩, symmetric_symmetrizeRel s,
symmetrizeRel_subset_self s⟩
