English
If (nhds 1) in G has a basis {b i} indexed by i ∈ I with basis sets b i, then (nhds 1) in UniformFun α G has a basis consisting of functions that stay in b i at every point; explicitly, the basis is {f : α →ᵤ G | ∀ x, f(x) ∈ b i}.
Русский
Если у (nhds 1) в G есть базис {b_i}, то (nhds 1) в UniformFun α G имеет базис из функций, которые во всех точках лежат в b_i: {f | ∀ x, f(x) ∈ b_i}.
LaTeX
$$$(\mathcal{nhds}(1)\text{ in } G)\HasBasis p b \Rightarrow (\mathcal{nhds}(1)\text{ in } (\mathrm{UniformFun} \; α \; G)).HasBasis p \big(i \mapsto \{f : α \to^\mathrm{u} G \mid \forall x, f(x) \in b i\}\big).$$$
Lean4
@[to_additive]
protected theorem hasBasis_nhds_one :
(𝓝 1 : Filter (α →ᵤ G)).HasBasis (fun V : Set G => V ∈ (𝓝 1 : Filter G)) fun V => {f : α → G | ∀ x, f x ∈ V} :=
UniformFun.hasBasis_nhds_one_of_basis (basis_sets _)
