hasBasis_symmetric — Mathlib

English

Symmetric entourages form a basis of 𝓤 α; i.e., (𝓤 α) has a basis consisting of symmetric relations.

Русский

Симметричные окружения образуют базис 𝓤 α.

LaTeX

$$$$(𝓤 α).HasBasis (\\lambda s: s \\in 𝓤 α \\wedge IsSymmetricRel s) id.$$$$

Lean4

/-- Symmetric entourages form a basis of `𝓤 α` -/
theorem hasBasis_symmetric : (𝓤 α).HasBasis (fun s : Set (α × α) => s ∈ 𝓤 α ∧ IsSymmetricRel s) id :=
  hasBasis_self.2 fun t t_in =>
    ⟨symmetrizeRel t, symmetrize_mem_uniformity t_in, symmetric_symmetrizeRel t, symmetrizeRel_subset_self t⟩

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