English
If 𝔖 is nonempty and directed, then the uniformity on α →ᵤ[𝔖] β has a HasBasis with nodes (S, i) where S ∈ 𝔖 and i indexes a basis for 𝓤 β, given by UniformOnFun.gen 𝔖 S (s i).
Русский
Если 𝔖 непусто и направлено, равномерность на α →ᵤ[𝔖] β имеет базис HasBasis с узлами (S, i), где S ∈ 𝔖 и i индексирует базис для 𝓤 β, заданный UniformOnFun.gen 𝔖 S (s i).
LaTeX
$$$\text{HasBasis }(\text{uniformity }(α→ᵤ[𝔖]β))\ { (S,i) } = UniformOnFun.gen 𝔖 S (s i).$$$
Lean4
/-- If `𝔖 : Set (Set α)` is nonempty and directed, then the uniformity of `α →ᵤ[𝔖] β` admits the
family `{(f, g) | ∀ x ∈ S, (f x, g x) ∈ V}` for `S ∈ 𝔖` and `V ∈ 𝓤 β` as a filter basis. -/
protected theorem hasBasis_uniformity (h : 𝔖.Nonempty) (h' : DirectedOn (· ⊆ ·) 𝔖) :
(𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun SV : Set α × Set (β × β) => SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓤 β) fun SV =>
UniformOnFun.gen 𝔖 SV.1 SV.2 :=
UniformOnFun.hasBasis_uniformity_of_basis α β 𝔖 h h' (𝓤 β).basis_sets
