English
If fr = fr1, then extendTo𝕜'(fr) = extendTo𝕜'(fr1).
Русский
Если fr = fr1, то extendTo𝕜'(fr) = extendTo𝕜'(fr1).
LaTeX
$$$fr = fr_1 \\Rightarrow \\ extendTo𝕜'(fr) = extendTo𝕜'(fr_1)$$$
Lean4
/-- Extend `fr : StrongDual ℝ F` to `StrongDual 𝕜 F`.
It would be possible to use `LinearMap.mkContinuous` here, but we would need to know that the
continuity of `fr` implies it has bounded norm and we want to avoid that dependency here.
Norm properties of this extension can be found in
`Mathlib/Analysis/Normed/Module/RCLike/Extend.lean`. -/
noncomputable def extendTo𝕜' (fr : StrongDual ℝ F) : StrongDual 𝕜 F
where
__ := fr.toLinearMap.extendTo𝕜'
cont := show Continuous fun x ↦ (fr x : 𝕜) - (I : 𝕜) * (fr ((I : 𝕜) • x) : 𝕜) by fun_prop
