English
If nhds 0 in F has a basis with index ι and family b, then the nhds of zero in E →SL[σ] F has a basis consisting of maps that are controlled on bounded subsets of E and by the basis b at each index.
Русский
Если у nhds(0) в F есть базис с индексами ι и семейство b, тогда nhds(0) в E →SL[σ] F имеет базис, задаваемый ограничением на ограниченных подмножеств E и по базису b для каждого индекса.
LaTeX
$$$$ (\mathcal{N}(0 : E \to_{σ} F)).HasBasis (\lambda SV: E \times ι, IsVonNBounded(SV.1) ∧ p(SV.2)) (\lambda SV, {f : E \to_{σ} F | \forall x ∈ SV.1, f(x) ∈ b(SV.2)}) $$$$
Lean4
instance continuousSMul [RingHomSurjective σ] [RingHomIsometric σ] [TopologicalSpace F] [IsTopologicalAddGroup F]
[ContinuousSMul 𝕜₂ F] : ContinuousSMul 𝕜₂ (E →SL[σ] F) :=
UniformConvergenceCLM.continuousSMul σ F {S | IsVonNBounded 𝕜₁ S} fun _ hs => hs
