Theorems · Theorem · general topology

UniformFun.isBasis_gen

∀ (α : Type u_1) (β : Type u_2) (𝓑 : Filter (β × β)), Filter.IsBasis (fun V => V ∈ 𝓑) (UniformFun.gen α β)

If 𝓕 is a filter on β × β, then the set of all UniformFun.gen α β V for V ∈ 𝓕 is a filter basis on (α →ᵤ β) × (α →ᵤ β). 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 15 from the axioms · uses Quot.sound