English
If β has a basis of uniformities, then the uniformity on α →ᵤ β has a corresponding basis obtained by composing that basis with the evaluation-acting part. In particular, 𝓤(α→ᵤβ) has basis obtained from a basis of 𝓤β via UniformFun.gen.
Русский
Если у β есть база равномерностей, то на α →ᵤ β база равномерности получается путем композиции этой базы с операцией UniformFun.gen.
LaTeX
$$$$\mathcal B(α,β) = \{ \mathrm{UniformFun.gen}(α,β,s_i) \}_{i} \text{ where } s_i \text{ run over a basis of } 𝓤β.$$$$
Lean4
/-- The uniformity of `α →ᵤ β` admits the family `{(f, g) | ∀ x, (f x, g x) ∈ V}` for `V ∈ 𝓑` as
a filter basis, for any basis `𝓑` of `𝓤 β` (in the case `𝓑 = (𝓤 β).as_basis` this is true by
definition). -/
protected theorem hasBasis_uniformity_of_basis {ι : Sort*} {p : ι → Prop} {s : ι → Set (β × β)}
(h : (𝓤 β).HasBasis p s) : (𝓤 (α →ᵤ β)).HasBasis p (UniformFun.gen α β ∘ s) :=
(UniformFun.hasBasis_uniformity α β).to_hasBasis
(fun _ hU =>
let ⟨i, hi, hiU⟩ := h.mem_iff.mp hU
⟨i, hi, fun _ huv x => hiU (huv x)⟩)
fun i hi => ⟨s i, h.mem_of_mem hi, subset_rfl⟩
