English
A variant asserting the HasBasis structure of the uniformity via a covering of 𝔖 by subfamilies t and a basis for β, yielding a basis for 𝓤(α→ᵤ[𝔖]β).
Русский
Вариант с HasBasis через покрытие 𝔖 подсемействами t и базой β, порождающий базис для 𝓤(α→ᵤ[𝔖]β).
LaTeX
$$$\text{HasBasis for } 𝓤(α→ᵤ[𝔖]β) \text{ given by } i=(t,i'), U_i = UniformOnFun.gen 𝔖 (t i.1) (V i.2).$$$
Lean4
/-- For `f : α →ᵤ[𝔖] β`, where `𝔖 : Set (Set α)` is nonempty and directed, `𝓝 f` admits the
family `{g | ∀ x ∈ S, (f x, g x) ∈ V}` for `S ∈ 𝔖` and `V ∈ 𝓤 β` as a filter basis. -/
protected theorem hasBasis_nhds (f : α →ᵤ[𝔖] β) (h : 𝔖.Nonempty) (h' : DirectedOn (· ⊆ ·) 𝔖) :
(𝓝 f).HasBasis (fun SV : Set α × Set (β × β) => SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓤 β) fun SV =>
{g | (g, f) ∈ UniformOnFun.gen 𝔖 SV.1 SV.2} :=
UniformOnFun.hasBasis_nhds_of_basis α β 𝔖 f h h' (Filter.basis_sets _)
