comp_comp_symm_mem_uniformity_sets

English

For s ∈ 𝓤 α, there exist t ∈ 𝓤 α with t symmetric and t ∘ t ∘ t ⊆ s.

Русский

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

LaTeX

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

Lean4

theorem comp_comp_symm_mem_uniformity_sets {s : Set (α × α)} (hs : s ∈ 𝓤 α) :
    ∃ t ∈ 𝓤 α, IsSymmetricRel t ∧ t ○ t ○ t ⊆ s :=
  by
  rcases comp_symm_mem_uniformity_sets hs with ⟨w, w_in, _, w_sub⟩
  rcases comp_symm_mem_uniformity_sets w_in with ⟨t, t_in, t_symm, t_sub⟩
  use t, t_in, t_symm
  have : t ⊆ t ○ t := subset_comp_self_of_mem_uniformity t_in
  calc
    t ○ t ○ t ⊆ w ○ (t ○ t) := by gcongr
    _ ⊆ w ○ w := by gcongr
    _ ⊆ s := w_sub

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