Theorems · Theorem · general topology

UniformFun.hasBasis_uniformity_of_basis

∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β] {ι : Sort u_5} {p : ι → Prop} {s : ι → Set (β × β)},
  (uniformity β).HasBasis p s → (uniformity (UniformFun α β)).HasBasis p (UniformFun.gen α β ∘ s)

The uniformity of α →ᵤ β admits the family {(f, g) | ∀ x, (f x, g x) ∈ V} for V ∈ 𝓑 as a filter basis, for any basis 𝓑 of 𝓤 β (in the case 𝓑 = (𝓤 β).as_basis this is true by definition).

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

8 results in Mathlib

Foundations

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

Assumes

UniformSpace