English
Let F be a topological vector space with a neighborhood basis of zero given by sets b(i) indexed by i in some index set. Then the space of continuous multilinear maps CM_k(E, F) has a neighborhood basis at zero consisting of sets defined by restricting these maps to send a von Neumann bounded input set into the corresponding basis neighborhood in F.
Русский
Пусть F — топологическое векторное пространство, у которого базис окрестностей нуля задаётся наборами b(i), индексируемыми i. Тогда пространство непрерывных много-линейных отображений CM_k(E, F) имеет базис окрестностей нуля, задаваемый наборами, которые требуют от отображаемых отображений отправлять von Neumann ограниченные входные множества во соответствующее окрестность нуля в F.
LaTeX
$$$\\mathrm{nhds}_{0}(\\mathrm{CM}_k(E,F))$ имеет базис из множеств вида $\\{f:\\prod_i E_i \\to F \\mid f(S) \\subseteq B\\}$, где $S$ — VonNBounded в $\\prod_i E_i$ и $B$ — окрестность нуля в $F$.$$
Lean4
theorem hasBasis_nhds_zero_of_basis {ι : Type*} {p : ι → Prop} {b : ι → Set F} (h : (𝓝 (0 : F)).HasBasis p b) :
(𝓝 (0 : ContinuousMultilinearMap 𝕜 E F)).HasBasis (fun Si : Set (Π i, E i) × ι => IsVonNBounded 𝕜 Si.1 ∧ p Si.2)
fun Si => {f | MapsTo f Si.1 (b Si.2)} :=
by
letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
rw [nhds_induced]
refine (UniformOnFun.hasBasis_nhds_zero_of_basis _ ?_ ?_ h).comap DFunLike.coe
· exact ⟨∅, isVonNBounded_empty _ _⟩
· exact directedOn_of_sup_mem fun _ _ => Bornology.IsVonNBounded.union
