English
Define eval: F → StrongDual 𝕜 (WeakBilin B) by eval(f) = (x ↦ B(x,f)) with appropriate linearity and topological properties.
Русский
Определим отображение оценки eval: F → StrongDual 𝕜 (WeakBilin B) таким образом, что eval(f)(x) = B(x,f) и проверить линейность и топологические свойства.
LaTeX
$$def eval [ContinousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] : F →ₗ[𝕜] StrongDual 𝕜 (WeakBilin B) where toFun f := ⟨B.flip f, by fun_prop⟩$$
Lean4
/-- Map `F` into the topological dual of `E` with the weak topology induced by `F`
-/
def eval [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] : F →ₗ[𝕜] StrongDual 𝕜 (WeakBilin B)
where
toFun f := ⟨B.flip f, by fun_prop⟩
map_add' _ _ := by ext; simp
map_smul' _ _ := by ext; simp
