English
Let 𝔖 be a nonempty directed family of subsets of E. Consider the space of uniform convergence on 𝔖 with values in F. The neighborhoods of the zero map are generated by prescribing, for a chosen subset S ∈ 𝔖 and a neighborhood V of 0 in F, that every map f sends all points of S into V.
Русский
Пусть 𝔖 непустое направленное семейство подмножеств E. Рассматриваем пространство равномерного сходства по каждому элементу 𝔖, со значениями в F. Окрестности нуля в этом пространстве образуют базис, задаваемый выбрав подмножество S ∈ 𝔖 и окрестность V вокруг 0 в F: для всех f выполняется f(x) ∈ V для всех x ∈ S.
LaTeX
$$$$ (\mathcal{N}(0 : \mathrm{UniformConvergenceCLM}_{\sigma} F \mathfrak{S})) \text{ has a basis } \{ SV = (S_E, S_F) : S_E \in \mathfrak{S},\ S_F \in (\mathcal{N}(0 : F)) \} \text{ consisting of } \{f : \mathrm{UniformConvergenceCLM}_{\sigma} F \mathfrak{S} \mid \forall x \in S_E, f(x) \in S_F\}.$$$$
Lean4
theorem hasBasis_nhds_zero [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) (h𝔖₁ : 𝔖.Nonempty)
(h𝔖₂ : DirectedOn (· ⊆ ·) 𝔖) :
(𝓝 (0 : UniformConvergenceCLM σ F 𝔖)).HasBasis (fun SV : Set E × Set F => SV.1 ∈ 𝔖 ∧ SV.2 ∈ (𝓝 0 : Filter F))
fun SV => {f : UniformConvergenceCLM σ F 𝔖 | ∀ x ∈ SV.1, f x ∈ SV.2} :=
hasBasis_nhds_zero_of_basis σ F 𝔖 h𝔖₁ h𝔖₂ (𝓝 0).basis_sets
