basis_uniformity — Mathlib

English

If α is a uniform space, the basis of the uniformity on the CauchyFilter extends from a basis of α via the gen operation.

Русский

Если α — равномерное пространство, база равномерности для CauchyFilter наследуется от базы α через операцию gen.

LaTeX

$$$ \forall {α} [\text{UniformSpace } α] {ι} {p} {s} (h : (\mathcal{U} α).HasBasis p s) : (\mathcal{U} (CauchyFilter α)).HasBasis p (gen \circ s)$$$

Lean4

theorem basis_uniformity {ι : Sort*} {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s) :
    (𝓤 (CauchyFilter α)).HasBasis p (gen ∘ s) :=
  h.lift' monotone_gen

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