norm_coe_norm — Mathlib

English

For any fr in StrongDual ℝ F and x in F, the norm of the extension to 𝕜' is bounded by the product of the operator norm of fr and the norm of x: ||fr.extendTo𝕜' x|| ≤ ||fr|| · ||x||.

Русский

Для любого fr из StrongDual ℝ F и любого x ∈ F имеем: ||fr.extendTo𝕜' x|| ≤ ||fr|| · ||x||.

LaTeX

$$$\\| (fr.extendTo𝕜'\\, x) \\| \\\\le \\\\|fr\\\\| \\\\cdot \\\\|x\\\\|$$$

Lean4

theorem norm_coe_norm {z : E} : ‖(‖z‖ : 𝕜)‖ = ‖z‖ := by simp

Похожие утверждения