English
For UniformConvergenceCLM, the space carries a natural structure as a class of continuous semilinear maps with respect to σ.
Русский
У UniformConvergenceCLM естественная структура как класс непрерывно полуплинейных отображений относительно σ.
LaTeX
$$$\\mathrm{ContinuousSemilinearMapClass}( \\mathrm{UniformConvergenceCLM}(\\sigma,F,\\mathcal{S}), \\sigma, E, F ).$$$
Lean4
/-- Given `E` and `F` two topological vector spaces and `𝔖 : Set (Set E)`, then
`UniformConvergenceCLM σ F 𝔖` is a type synonym of `E →SL[σ] F` equipped with the "topology of
uniform convergence on the elements of `𝔖`".
If the continuous linear image of any element of `𝔖` is bounded, this makes `E →SL[σ] F` a
topological vector space. -/
@[nolint unusedArguments]
def UniformConvergenceCLM [TopologicalSpace F] (_ : Set (Set E)) :=
E →SL[σ] F
