Theorems · Theorem · general topology

UniformOnFun.uniformity_eq_of_basis

∀ {α : Type u_1} (β : Type u_2) [inst : UniformSpace β] (𝔖 : Set (Set α)) {ι : Sort u_5} {p : ι → Prop}
  {V : ι → Set (β × β)},
  (uniformity β).HasBasis p V →
    uniformity (UniformOnFun α β 𝔖) = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), Filter.principal (UniformOnFun.gen 𝔖 s (V i))

A version of UniformOnFun.hasBasis_uniformity_of_basis with weaker conclusion and weaker assumptions. We make no assumptions about the set 𝔖 but conclude only that the uniformity is equal to some indexed infimum.

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpace