English
The neighborhood of zero in UniformConvergenceCLM σ F 𝔖 is the infimum, over s ∈ 𝔖 and t ∈ 𝓝(0) in F, of the principal filters on the sets { f : UniformConvergenceCLM σ F 𝔖 | MapsTo f s t }.
Русский
Окрестность нуля в UniformConvergenceCLM σ F 𝔖 равна пересечению (наименьшему верхнему пределу) по всем s ∈ 𝔖 и t ∈ 𝓝(0) в F множества { f : UniformConvergenceCLM σ F 𝔖 | MapsTo f s t }.
LaTeX
$$$$ \mathcal{N}(0 : UniformConvergenceCLM_{\sigma} F \mathfrak{S}) = \bigwedge_{s \in \mathfrak{S}} \bigwedge_{t \in \mathcal{N}(0)} \mathcal{P}\{ f : \mathrm{UniformConvergenceCLM}_{\sigma} F \mathfrak{S} \mid MapsTo(f, s, t) \}. $$$$
Lean4
theorem nhds_zero_eq [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) :
𝓝 (0 : UniformConvergenceCLM σ F 𝔖) =
⨅ s ∈ 𝔖, ⨅ t ∈ 𝓝 (0 : F), 𝓟 {f : UniformConvergenceCLM σ F 𝔖 | MapsTo f s t} :=
nhds_zero_eq_of_basis _ _ _ (𝓝 0).basis_sets
