Theorems · Theorem · general topology

UniformOnFun.nhds_eq

∀ {α : Type u_1} (β : Type u_2) [inst : UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖),
  nhds f =
    ⨅ s ∈ 𝔖,
      ⨅ V ∈ uniformity β, Filter.principal {g | ∀ x ∈ s, ((UniformOnFun.toFun 𝔖) f x, (UniformOnFun.toFun 𝔖) g x) ∈ V}

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpace