Theorems · Definition · general topology

UniformFun.basis

(α : Type u_1) → (β : Type u_2) → Filter (β × β) → FilterBasis (UniformFun α β × UniformFun α β)

For 𝓕 : Filter (β × β), this is the set of all UniformFun.gen α β V for V ∈ 𝓕 as a bundled FilterBasis over (α →ᵤ β) × (α →ᵤ β). This will only be applied to 𝓕 = 𝓤 β when β is equipped with a UniformSpace structure, but it is useful to define it for any filter in order to be able to state that it has a lower adjoint (see UniformFun.gc).

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

1 results in Mathlib

Foundations

Depth 16 from the axioms · uses Quot.sound