comp_open_symm_mem_uniformity_sets

English

For any entourage s, there exists an open symmetric t with t○t ⊆ s.

Русский

Для любого энтурджа s существует открытый симметричный t, такой что t○t ⊆ s.

LaTeX

$$$\exists t ∈ 𝓤 α, IsOpen t ∧ IsSymmetricRel t ∧ t \circ t ⊆ s$$$

Lean4

theorem comp_open_symm_mem_uniformity_sets {s : Set (α × α)} (hs : s ∈ 𝓤 α) :
    ∃ t ∈ 𝓤 α, IsOpen t ∧ IsSymmetricRel t ∧ t ○ t ⊆ s :=
  by
  obtain ⟨t, ht₁, ht₂⟩ := comp_mem_uniformity_sets hs
  obtain ⟨u, ⟨hu₁, hu₂, hu₃⟩, hu₄ : u ⊆ t⟩ := uniformity_hasBasis_open_symmetric.mem_iff.mp ht₁
  exact ⟨u, hu₁, hu₂, hu₃, (compRel_mono hu₄ hu₄).trans ht₂⟩

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