English
The range of the map toUniformOnFun is exactly the set of UniformOnFun objects that arise from continuous multilinear maps, i.e., they are exactly those f for which the underlying function is continuous and is multilinearly additive in each argument and homogeneous in scalars.
Русский
Область значений отображения toUniformOnFun совпадает с множеством UniformOnFun, соответствующих непрерывным мультилинеарным отображениям; т.е. такие f имеют непрерывную подстановку и билинейную аддитивность в каждом аргументе и однородность по скалярам.
LaTeX
$$$\text{Range}(\text{toUniformOnFun}) = \{ f : (Π i, E_i) →_u[{s \;|\; IsVonNBounded 𝕜 s}] F \\| \\text{Continuous}(toFun\, f) \\wedge \\forall m,i,x,y,\toFun f (update m i (x+y)) = toFun f (update m i x) + toFun f (update m i y) \\wedge \\forall m,i,c,x, toFun f (update m i (c \cdot x)) = c \cdot toFun f (update m i x) \} $$$
Lean4
/-- An auxiliary definition used to define topology on `ContinuousMultilinearMap 𝕜 E F`. -/
def toUniformOnFun [TopologicalSpace F] (f : ContinuousMultilinearMap 𝕜 E F) :
(Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F :=
UniformOnFun.ofFun _ f
