comp_mem_uniformity_sets — Mathlib

English

Let c be a UniformSpace.Core on α. If s is an element of c.uniformity, then there exists a t ∈ c.uniformity with t ○ t ⊆ s.

Русский

Пусть c — Core равномерного пространства на α. Если s ∈ c.uniformity, существует t ∈ c.uniformity такое, что t ○ t ⊆ s.

LaTeX

$$$\\forall {\\alpha} {c : UniformSpace.Core\\,\\alpha}\\, \\forall s \\in c.uniformity,\n\\;\\exists t \\in c.uniformity, t \\circ t \\subseteq s$$$

Lean4

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

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