hasBasis_uniformity — Mathlib

English

The uniformity on α →ᵤ β has as a basis the family of sets { (f,g) : ∀ x, (f x, g x) ∈ V } with V ranging over the uniformity 𝓤β of β.

Русский

Унитормность на α →ᵤ β имеет базис в виде множеств { (f,g) : ∀ x, (f(x), g(x)) ∈ V } для V из 𝓤β.

LaTeX

$$$${\mathcal U}(\alpha, \beta) \text{ has a basis } \{ (f,g) : \forall x, (f(x), g(x)) \in V \} \text{ for all } V \in 𝓤(β).$$$$

Lean4

/-- By definition, the uniformity of `α →ᵤ β` admits the family `{(f, g) | ∀ x, (f x, g x) ∈ V}`
for `V ∈ 𝓤 β` as a filter basis. -/
protected theorem hasBasis_uniformity : (𝓤 (α →ᵤ β)).HasBasis (· ∈ 𝓤 β) (UniformFun.gen α β) :=
  (UniformFun.isBasis_gen α β (𝓤 β)).hasBasis

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