mem_uniformity — Mathlib

English

The uniformity on CauchyFilter α is generated by sets of the form gen(t) with t ∈ 𝓤 α.

Русский

Унитарность на CauchyFilter α образуется из множеств gen(t) при t ∈ 𝓤 α.

LaTeX

$$$s\\in 𝓤(CauchyFilter(\\alpha))\\iff \\exists t\\in 𝓤(\\alpha),\\ \\mathrm{gen}(t)\\subseteq s$$$

Lean4

theorem mem_uniformity {s : Set (CauchyFilter α × CauchyFilter α)} : s ∈ 𝓤 (CauchyFilter α) ↔ ∃ t ∈ 𝓤 α, gen t ⊆ s :=
  mem_lift'_sets monotone_gen

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