Theorems · Definition · general topology

UniformFun.filter

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

For 𝓕 : Filter (β × β), this is the filter generated by the filter basis UniformFun.basis α β 𝓕. For 𝓕 = 𝓤 β, this will be the uniformity of uniform convergence on α.

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

2 results in Mathlib

Foundations

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