∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {ι : Type u_1} {p : ι → Prop}
  {V : ι → Set (β × β)} (K : CompactExhaustion α),
  (uniformity β).HasBasis p V →
    (uniformity C(α, β)).HasBasis (fun i => p i.2) fun i => {fg | ∀ x ∈ K i.1, (fg.1 x, fg.2 x) ∈ V i.2}