Theorems · Theorem · general topology

UniformFun.hasBasis_uniformity

∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β],
  (uniformity (UniformFun α β)).HasBasis (fun x => x ∈ uniformity β) (UniformFun.gen α β)

By definition, the uniformity of α →ᵤ β admits the family {(f, g) | ∀ x, (f x, g x) ∈ V} for V ∈ 𝓤 β as a filter basis.

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

12 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

UniformSpace