English
Let 𝔖 be a nonempty directed family of subsets of α. If (nhds 1 : Filter G) has a basis {p,i}, then (nhds 1 : Filter (UniformOnFun α G 𝔖)) has a basis indexed by 𝔖 × ι with elements {f : α →ᵤ[𝔖] G | ∀ x ∈ S, f(x) ∈ b i}.
Русский
Пусть 𝔖 — непустое направленное семейство подмножеств α. Если (nhds 1) в G имеет базис {p,i}, то (nhds 1) в UniformOnFun α G 𝔖 имеет базис, индексированный 𝔖 × ι, состоящий из наборов {f | ∀ x ∈ S, f(x) ∈ b i}.
LaTeX
$$$(\mathcal{nhds}(1)\ in G) \Rightarrow (\mathcal{nhds}(1)\ in (\mathrm{UniformOnFun} \; α \; G \; 𝔖))$ имеет Basis, заданный таким образом: $(Si \in 𝔖, pSi)$ и соответствующая функцияобразная. $$
Lean4
@[to_additive]
protected theorem hasBasis_nhds_one_of_basis (𝔖 : Set <| Set α) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (· ⊆ ·) 𝔖)
{p : ι → Prop} {b : ι → Set G} (h : (𝓝 1 : Filter G).HasBasis p b) :
(𝓝 1 : Filter (α →ᵤ[𝔖] G)).HasBasis (fun Si : Set α × ι => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si =>
{f : α →ᵤ[𝔖] G | ∀ x ∈ Si.1, toFun 𝔖 f x ∈ b Si.2} :=
by
convert UniformOnFun.hasBasis_nhds_of_basis α _ 𝔖 (1 : α →ᵤ[𝔖] G) h𝔖₁ h𝔖₂ <| h.uniformity_of_nhds_one_swapped
simp [UniformOnFun.gen]
