toSpanNonzeroSingleton_homothety — Mathlib

English

Let x be a nonzero element of a normed space E over 𝕜. The natural linear isomorphism from 𝕜 to the span of x, given by c ↦ c x, is a homothety with factor ||x||; in particular, for all c ∈ 𝕜, ∥c x∥ = ∥x∥ · ∥c∥.

Русский

Пусть x ≠ 0 — ненулевой вектор в нормированном пространстве E над полем 𝕜. Естественное линейное взаимно однозначное отображение 𝕜 на линейное пространство 𝕜·x, заданное c ↦ c x, является гомотетией с коэффициентом ||x||; следовательно, для каждого c ∈ 𝕜 выполняется ∥c x∥ = ∥x∥ · ∥c∥.

LaTeX

$$$\\exists T:\\mathbb{K} \\to_L\\mathbb{K}\\cdot x,\\; T(c)=c x\\;\\wedge\\; \\|T\\|=\\|x\\|$$$

Lean4

theorem _root_.LinearEquiv.toSpanNonzeroSingleton_homothety (x : E) (h : x ≠ 0) (c : 𝕜) :
    ‖LinearEquiv.toSpanNonzeroSingleton 𝕜 E x h c‖ = ‖x‖ * ‖c‖ :=
  LinearMap.toSpanSingleton_homothety _ _ _

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