symm_of_uniformity — Mathlib

English

Given s ∈ 𝓤 α, there exists t ∈ 𝓤 α such that t is symmetric and t ⊆ s.

Русский

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

LaTeX

$$$$\\forall s ∈ 𝓤 α,\\; ∃ t ∈ 𝓤 α:\\ (\\forall a b, (a,b) ∈ t \\Rightarrow (b,a) ∈ t) ∧ t ⊆ s.$$$$

Lean4

theorem symm_of_uniformity {s : Set (α × α)} (hs : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, (∀ a b, (a, b) ∈ t → (b, a) ∈ t) ∧ t ⊆ s :=
  have : preimage Prod.swap s ∈ 𝓤 α := symm_le_uniformity hs
  ⟨s ∩ preimage Prod.swap s, inter_mem hs this, fun _ _ ⟨h₁, h₂⟩ => ⟨h₂, h₁⟩, inter_subset_left⟩

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