toSpanSingleton_homothety — Mathlib

English

For a vector x and scalar c, the norm of the span singleton map equals the product of the norms: ||toSpanSingleton(x)c|| = ||x|| · ||c||.

Русский

Для вектора x и скаляра c нормa линейного отображения в SpanSingleton равна произведению норм: ||toSpanSingleton(x)c|| = ||x|| · ||c||.

LaTeX

$$$$ \|\text{toSpanSingleton}(x)\,c\| = \|x\| \cdot \|c\|. $$$$

Lean4

theorem toSpanSingleton_homothety (x : E) (c : 𝕜) : ‖LinearMap.toSpanSingleton 𝕜 E x c‖ = ‖x‖ * ‖c‖ :=
  by
  rw [mul_comm]
  exact norm_smul _ _

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