comp_symm_mem_uniformity_sets — Mathlib

English

For s ∈ 𝓤 α, there exists t ∈ 𝓤 α such that IsSymmetricRel t and t ∘ t ⊆ s.

Русский

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

LaTeX

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

Lean4

/-- See also `comp_open_symm_mem_uniformity_sets`. -/
theorem comp_symm_mem_uniformity_sets {s : Set (α × α)} (hs : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, IsSymmetricRel t ∧ t ○ t ⊆ s :=
  by
  obtain ⟨w, w_in, w_sub⟩ : ∃ w ∈ 𝓤 α, w ○ w ⊆ s := comp_mem_uniformity_sets hs
  use symmetrizeRel w, symmetrize_mem_uniformity w_in, symmetric_symmetrizeRel w
  have : symmetrizeRel w ⊆ w := symmetrizeRel_subset_self w
  calc
    symmetrizeRel w ○ symmetrizeRel w
    _ ⊆ w ○ w := by gcongr
    _ ⊆ s := w_sub

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