hasBasis_uniformity — Mathlib

English

The uniformity 𝓤[abv.uniformSpace] has a basis given by neighborhoods defined by abv on differences, i.e., sets { (p,q) : abv(q−p) < ε } for ε > 0.

Русский

Униформность 𝓤[abv.uniformSpace] обладает базисом, задаваемым окрестностями { (p,q) : abv(q−p) < ε } при ε > 0.

LaTeX

$$$\\mathcal U[abv.uniformSpace] .HasBasis (0 < ·) (\\varepsilon \\mapsto \\{(p,q)\\in R\\times R : abv(q-p) < \\varepsilon\\})$$$

Lean4

theorem hasBasis_uniformity : 𝓤[abv.uniformSpace].HasBasis ((0 : 𝕜) < ·) fun ε => {p : R × R | abv (p.2 - p.1) < ε} :=
  UniformSpace.hasBasis_ofFun (exists_gt _) _ _ _ _ _

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