toSpanUnitSingleton — Mathlib

English

If x is a unit vector (∥x∥ = 1), there is a linear isometry between 𝕜 and 𝕜·x, i.e., a 𝕜-linear isometry equivalence.

Русский

Если x — единичный вектор (∥x∥ = 1), существует линейный изометрический эквивалент между 𝕜 и 𝕜·x.

LaTeX

$$$\\exists x:\\mathbb{K}^n \\text{ с } \\|x\\|=1:\\; 𝕜 \\simeq_{L,\\,\\; isometry} 𝕜\\cdot x$$$

Lean4

/-- Given a unit element `x` of a normed space `E` over a field `𝕜`, the natural
linear isometry equivalence from `𝕜` to the span of `x`. -/
noncomputable def toSpanUnitSingleton (x : E) (hx : ‖x‖ = 1) : 𝕜 ≃ₗᵢ[𝕜] 𝕜 ∙ x
    where
  toLinearEquiv := LinearEquiv.toSpanNonzeroSingleton 𝕜 E x (by aesop)
  norm_map' := by
    intro
    rw [LinearEquiv.toSpanNonzeroSingleton_homothety, hx, one_mul]

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