English
For any nonempty 𝔖 and directed 𝔖, the neighborhood basis at 1 in UniformOnFun α G 𝔖 is given by pairs SV = (S, i) with S ∈ 𝔖 and i in the index set, and the basic neighborhoods consist of functions f with f(x) ∈ V for all x ∈ S where V ∈ nhds 1 in G.
Русский
Для любого непустого 𝔖 и направленного 𝔖 базис окрестностей 1 в UniformOnFun α G 𝔖 задается парами SV = (S, i) с S ∈ 𝔖 и i в индексе, базовые окрестности состоят из функций f с f(x) ∈ V для всех x ∈ S, где V ∈ nhds 1 в G.
LaTeX
$$$(\mathcal{nhds}(1)\; (\alpha \to^\mathrm{u} G))\HasBasis (\lambda SV: SV \in 𝔖) (\lambda SV => {f : α →ᵤ[𝔖] G | ∀ x ∈ SV.1, f(x) ∈ SV.2}).$$$
Lean4
@[to_additive]
protected theorem hasBasis_nhds_one (𝔖 : Set <| Set α) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (· ⊆ ·) 𝔖) :
(𝓝 1 : Filter (α →ᵤ[𝔖] G)).HasBasis (fun SV : Set α × Set G => SV.1 ∈ 𝔖 ∧ SV.2 ∈ (𝓝 1 : Filter G)) fun SV =>
{f : α →ᵤ[𝔖] G | ∀ x ∈ SV.1, f x ∈ SV.2} :=
UniformOnFun.hasBasis_nhds_one_of_basis 𝔖 h𝔖₁ h𝔖₂ (basis_sets _)
