English
If the space F has a neighborhood basis at 0 given by a family p i with sets b i, then the neighborhood of 0 in UniformConvergenceCLM σ F 𝔖 is the infimum of principal filters over all s ∈ 𝔖 and i with p i, of the sets { f : UniformConvergenceCLM σ F 𝔖 | MapsTo f s b i }.
Русский
Если у пространства F имеется базис окрестностей нуля, заданный семейством p i со множествами b i, то окрестности нуля в UniformConvergenceCLM σ F 𝔖 равны наименьшему (пересечению) фильтров, взятым по всем s ∈ 𝔖 и i, удовлетворяющим p i, от множества { f : UniformConvergenceCLM σ F 𝔖 | MapsTo f s b i }.
LaTeX
$$$$ \mathcal{N}(0 : UniformConvergenceCLM_{\sigma} F \mathfrak{S}) = \bigwedge_{s \in \mathfrak{S}} \bigwedge_{i: ι,\ p(i)} \mathcal{P}\{ f : \mathrm{UniformConvergenceCLM}_{\sigma} F \mathfrak{S} \mid MapsTo(f, s, b(i)) \}.$$$$
Lean4
theorem nhds_zero_eq_of_basis [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) {ι : Type*}
{p : ι → Prop} {b : ι → Set F} (h : (𝓝 0 : Filter F).HasBasis p b) :
𝓝 (0 : UniformConvergenceCLM σ F 𝔖) =
⨅ (s : Set E) (_ : s ∈ 𝔖) (i : ι) (_ : p i), 𝓟 {f : UniformConvergenceCLM σ F 𝔖 | MapsTo f s (b i)} :=
by
letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
rw [(isEmbedding_coeFn σ F 𝔖).isInducing.nhds_eq_comap, UniformOnFun.nhds_eq_of_basis _ _ h.uniformity_of_nhds_zero]
simp [MapsTo]
