English
Another articulation of the range description for UniformOnFun corresponding to continuous multilinear maps, matching the previous characterization with the same structure.
Русский
Ещё одно изложение диапазона UniformOnFun, соответствующее непрерывным мультилинеарным отображениям, аналогично предыдущему описанию.
LaTeX
$$$\text{Range}(\text{toUniformOnFun}) = \{ f : (Π i, E_i) →_u[{s \;|\; IsVonNBounded 𝕜 s}] F \| \text{...} \}$$$
Lean4
theorem range_toUniformOnFun [DecidableEq ι] [TopologicalSpace F] :
range toUniformOnFun =
{f : (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F |
Continuous (toFun _ f) ∧
(∀ (m : Π i, E i) i x y,
toFun _ f (update m i (x + y)) = toFun _ f (update m i x) + toFun _ f (update m i y)) ∧
(∀ (m : Π i, E i) i (c : 𝕜) x, toFun _ f (update m i (c • x)) = c • toFun _ f (update m i x))} :=
by
ext f
constructor
· rintro ⟨f, rfl⟩
exact ⟨f.cont, f.map_update_add, f.map_update_smul⟩
· rintro ⟨hcont, hadd, hsmul⟩
exact ⟨⟨⟨f, by intro; convert hadd, by intro; convert hsmul⟩, hcont⟩, rfl⟩
