norm_toSpanSingleton — Mathlib

English

The norm of the span singleton of a vector equals the norm of the vector itself, reflecting the preservation of norm under the span operation.

Русский

Норма одноэлементного образа единичного интервалa совпадает с нормой вектора, что отражает сохранение нормы при операции span.

LaTeX

$$$\|toSpanSingleton\;x\| = \|x\|$$$

Lean4

theorem norm_toSpanSingleton (x : E) : ‖toSpanSingleton 𝕜 x‖ = ‖x‖ :=
  by
  refine opNorm_eq_of_bounds (norm_nonneg _) (fun x => ?_) fun N _ h => ?_
  · rw [toSpanSingleton_apply, norm_smul, mul_comm]
  · simpa [toSpanSingleton_apply, norm_smul] using h 1

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