Theorems · Definition · general topology

UniformOnFun.gen

{α : Type u_1} →
  {β : Type u_2} → (𝔖 : Set (Set α)) → Set α → Set (β × β) → Set (UniformOnFun α β 𝔖 × UniformOnFun α β 𝔖)

Basis sets for the uniformity of 𝔖-convergence: for S : Set α and V : Set (β × β), gen 𝔖 S V is the set of pairs (f, g) of functions α →ᵤ[𝔖] β such that ∀ x ∈ S, (f x, g x) ∈ V. Note that the family 𝔖 : Set (Set α) is only used to specify which type alias of α → β to use here.

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

18 results in Mathlib

Foundations

Depth 14 from the axioms · uses Quot.sound