Theorems · Theorem · general topology

UniformOnFun.nhds_eq_of_basis

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

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

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpace