comp_mem_uniformity_sets — Mathlib

English

Let s be an entourage in 𝓤 α. Then there exists an entourage t ∈ 𝓤 α such that t ∘ t ⊆ s.

Русский

Пусть s ∈ 𝓤 α. Существуют t ∈ 𝓤 α такие, что t ∘ t ⊆ s.

LaTeX

$$$$\\forall s \\in 𝓤\\alpha,\\; \\exists t \\in 𝓤\\alpha,\\; t \\circ t \\subseteq s.$$$$

Lean4

theorem comp_mem_uniformity_sets {s : Set (α × α)} (hs : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, t ○ t ⊆ s :=
  (mem_lift'_sets <| monotone_id.compRel monotone_id).mp <| comp_le_uniformity hs

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