English
A real-linear StrongDual can be extended to a 𝕜-linear StrongDual via a canonical extension which preserves linearity and continuity properties.
Русский
Двойственное отображение с действием по реальным координатам может быть расширено до 𝕜-линейного сильного двойственного отображения, сохраняя линейность и непрерывность.
LaTeX
$$$\text{extendTo𝕜'ℓ}: \mathrm{StrongDual}_{\mathbb{R}} E \to \mathrm{StrongDual}_{𝕜} E$ является линейным отображением$$
Lean4
/-- Real linear extension of continuous extension of `LinearMap.extendTo𝕜'` -/
noncomputable def extendTo𝕜'ₗ [ContinuousConstSMul 𝕜 E] : StrongDual ℝ E →ₗ[ℝ] StrongDual 𝕜 E :=
letI to𝕜 (fr : StrongDual ℝ E) : StrongDual 𝕜 E :=
{ toLinearMap := LinearMap.extendTo𝕜' fr
cont := show Continuous fun x ↦ (fr x : 𝕜) - (I : 𝕜) * (fr ((I : 𝕜) • x) : 𝕜) by fun_prop }
have h fr x : to𝕜 fr x = ((fr x : 𝕜) - (I : 𝕜) * (fr ((I : 𝕜) • x) : 𝕜)) := rfl
{ toFun := to𝕜
map_add' := by intros; ext; simp [h]; ring
map_smul' := by intros; ext; simp [h, real_smul_eq_coe_mul]; ring }
