Theorems · Definition · functional analysis

LinearIsometry.toSpanSingleton

(𝕜 : Type u_1) →
  (E : Type u_4) →
    [inst : SeminormedAddCommGroup E] →
      [inst_1 : NontriviallyNormedField 𝕜] → [inst_2 : NormedSpace 𝕜 E] → {v : E} → ‖v‖ = 1 → 𝕜 →ₗᵢ[𝕜] E

Given a unit-length element x of a normed space E over a field 𝕜, the natural linear isometry map from 𝕜 to E by taking multiples of x.

Defined in

Mathlib.Analysis.Normed.Operator.Basic

Cited by

6 results in Mathlib

Foundations

Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedAddCommGroupNontriviallyNormedFieldNormedSpace