English
For a nonzero x in a normed space E over 𝕜, there exists a continuous linear isomorphism from 𝕜 to the span of x, taking c to c x, with operator norm equal to ∥x∥.
Русский
Для ненулевого вектора x в нормированном пространстве E над 𝕜 существует непрерывный линейный изоморфизм от 𝕜 к span{x}, отображающий c ↦ c x, с нормой оператора равной ∥x∥.
LaTeX
$$$\\exists T:\\mathbb{K}\\to_L[\\mathbb{K}]\\mathbb{K}\\cdot x,\\; T(c)=c x,\\; \\|T\\|=\\|x\\|$$$
Lean4
/-- Given a nonzero element `x` of a normed space `E₁` over a field `𝕜`, the natural
continuous linear equivalence from `𝕜` to the span of `x`. -/
@[simps!]
noncomputable def toSpanNonzeroSingleton (x : E) (h : x ≠ 0) : 𝕜 ≃L[𝕜] 𝕜 ∙ x :=
ofHomothety (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x h) ‖x‖ (norm_pos_iff.mpr h)
(LinearEquiv.toSpanNonzeroSingleton_homothety 𝕜 x h)
