English
There is a canonical embedding from WeakBilin B into the strong dual, via the map f ↦ (y ↦ B(f,y)) or via B.flip; this identifies f with a continuous linear functional on WeakBilin B.
Русский
Существует каноническое встраивание WeakBilin B в сильный двойственный пространство через f ↦ (y ↦ B(f,y)) (или через B.flip); таким образом f соответствует непрерывному линейному функционалу на WeakBilin B.
LaTeX
$$embedding of WeakBilin B into StrongDual via B$$
Lean4
/-- Scalar multiplication by `𝕜` on `WeakBilin B` is continuous. -/
instance instContinuousSMul [ContinuousSMul 𝕜 𝕜] : ContinuousSMul 𝕜 (WeakBilin B) :=
by
refine ⟨continuous_induced_rng.2 ?_⟩
refine cast (congr_arg _ ?_) (continuous_fst.smul ((coeFn_continuous B).comp continuous_snd))
ext
simp only [Function.comp_apply, Pi.smul_apply, LinearMap.map_smulₛₗ, RingHom.id_apply, LinearMap.smul_apply]
