English
There is an algebra-homomorphism forgetting that a bounded continuous function is bounded, i.e., from α →ᵇ γ to the bounded continuous maps C(α, γ).
Русский
Существует алгебрографоморфизм, забывающий ограниченность, т. е. из α →ᵇ γ в C(α, γ).
LaTeX
$$$\\text{toContinuousMap}: (α \\to^b γ) \\to_𝕜 C(α, γ)$$$
Lean4
instance instModule' : Module (α →ᵇ 𝕜) (α →ᵇ β) :=
Module.ofMinimalAxioms (fun c _ _ => ext fun a => smul_add (c a) _ _) (fun _ _ _ => ext fun _ => add_smul _ _ _)
(fun _ _ _ => ext fun _ => mul_smul _ _ _)
(fun f => ext fun x => one_smul 𝕜 (f x))
/- TODO: When `NormedModule` has been added to `Analysis.Normed.Module.Basic`, this
shows that the space of bounded continuous functions from `α` to `β` is naturally a normed
module over the algebra of bounded continuous functions from `α` to `𝕜`. -/
