isClopen_ball_of_isSymmetricRel_of_isTransitiveRel_of_mem_uniformity

English

If a uniform space X has a basis of entourages with symmetric and transitive members, then X is ultra uniform.

Русский

Если 𝓤X имеет базис окружений, члены которого симметричны и транзитивны, то X является ультра-однородным.

LaTeX

$$( (𝓤 X).HasBasis p s ∧ ∀ i, p i → IsSymmetricRel (s i) ∧ IsTransitiveRel (s i) ) ⇒ IsUltraUniformity X$$

Lean4

theorem isClopen_ball_of_isSymmetricRel_of_isTransitiveRel_of_mem_uniformity (x : X) {V : Set (X × X)}
    (h_symm : IsSymmetricRel V) (h_trans : IsTransitiveRel V) (h' : V ∈ 𝓤 X) : IsClopen (ball x V) :=
  ⟨isClosed_ball_of_isSymmetricRel_of_isTransitiveRel_of_mem_uniformity _ ‹_› ‹_› ‹_›,
    h_trans.isOpen_ball_of_mem_uniformity _ ‹_›⟩

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