ContinuousLinearMap.norm_extendTo𝕜'_bound

theorem ContinuousLinearMap.norm_extendTo𝕜'_bound : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : SeminormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedSpace ℝ F] [inst_4 : IsScalarTower ℝ 𝕜 F] (fr : F →L[ℝ] ℝ) (x : F), ‖fr.extendTo𝕜' x‖ ≤ ‖fr‖ * ‖x‖

This theorem states that for a given continuous linear map `fr` from a seminormed add commutative group `F`, which is also a normed space over ℝ and 𝕜, with ℝ being a scalar tower over 𝕜 and `F`, and a given element `x` in `F`, the norm of the extension of `fr` to 𝕜 denoted by `fr.extendTo𝕜' x` is bounded above by the product of the norm of `fr` and the norm of `x`. In mathematical terms, it's expressed as ‖fr.extendTo𝕜' x‖ ≤ ‖fr‖ * ‖x‖.

More concisely: For a continuous linear map `fr` from a seminormed add commutative group `F` into ℝ, and an element `x` in `F`, the norm of the extension of `fr` to `ℝ[X]` (denoted `fr.extendTo𝕜' x`) is bounded above by the product of the norm of `fr` and the norm of `x`. In other words, ‖`fr.extendTo𝕜' x`‖ ≤ ‖`fr`‖ * ‖`x`‖.