comp_symm_of_uniformity — Mathlib

English

There exists a symmetric t ∈ 𝓤 α with t ∘ t ⊆ s for any s ∈ 𝓤 α.

Русский

Для любого s ∈ 𝓤 α существует симметричное t ∈ 𝓤 α такое, что t ∘ t ⊆ s.

LaTeX

$$$$\\forall s ∈ 𝓤 α, \\exists t ∈ 𝓤 α:\\ IsSymmetricRel t ∧ t ◦ t ⊆ s.$$$$

Lean4

theorem comp_symm_of_uniformity {s : Set (α × α)} (hs : s ∈ 𝓤 α) :
    ∃ t ∈ 𝓤 α, (∀ {a b}, (a, b) ∈ t → (b, a) ∈ t) ∧ t ○ t ⊆ s :=
  let ⟨_t, ht₁, ht₂⟩ := comp_mem_uniformity_sets hs
  let ⟨t', ht', ht'₁, ht'₂⟩ := symm_of_uniformity ht₁
  ⟨t', ht', ht'₁ _ _, Subset.trans (monotone_id.compRel monotone_id ht'₂) ht₂⟩

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