# The span of a single vector #

The equivalence of ๐ and ๐ โข x for x โ  0 are defined as continuous linear equivalence and isometry.

## Main definitions #

• ContinuousLinearEquiv.toSpanNonzeroSingleton: The continuous linear equivalence between ๐ and ๐ โข x for x โ  0.
• LinearIsometryEquiv.toSpanUnitSingleton: For โxโ = 1 the continuous linear equivalence is a linear isometry equivalence.
theorem LinearMap.toSpanSingleton_homothety (๐ : Type u_1) {E : Type u_2} [] [Module ๐ E] [BoundedSMul ๐ E] (x : E) (c : ๐) :
theorem LinearEquiv.toSpanNonzeroSingleton_homothety (๐ : Type u_1) {E : Type u_2} [] [Module ๐ E] [BoundedSMul ๐ E] (x : E) (h : x โ  0) (c : ๐) :
noncomputable def ContinuousLinearEquiv.toSpanNonzeroSingleton (๐ : Type u_1) {E : Type u_2} [NormedField ๐] [NormedSpace ๐ E] (x : E) (h : x โ  0) :
๐ โL[๐] โฅ(Submodule.span ๐ {x})

Given a nonzero element x of a normed space Eโ over a field ๐, the natural continuous linear equivalence from Eโ to the span of x.

Equations
Instances For
noncomputable def ContinuousLinearEquiv.coord (๐ : Type u_1) {E : Type u_2} [NormedField ๐] [NormedSpace ๐ E] (x : E) (h : x โ  0) :
โฅ(Submodule.span ๐ {x}) โL[๐] ๐

Given a nonzero element x of a normed space Eโ over a field ๐, the natural continuous linear map from the span of x to ๐.

Equations
• = โ().symm
Instances For
@[simp]
theorem ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm (๐ : Type u_1) {E : Type u_2} [NormedField ๐] [NormedSpace ๐ E] {x : E} (h : x โ  0) :
โ().symm = โ()
@[simp]
theorem ContinuousLinearEquiv.coord_toSpanNonzeroSingleton (๐ : Type u_1) {E : Type u_2} [NormedField ๐] [NormedSpace ๐ E] {x : E} (h : x โ  0) (c : ๐) :
() (() c) = c
@[simp]
theorem ContinuousLinearEquiv.toSpanNonzeroSingleton_coord (๐ : Type u_1) {E : Type u_2} [NormedField ๐] [NormedSpace ๐ E] {x : E} (h : x โ  0) (y : โฅ(Submodule.span ๐ {x})) :
() (() y) = y
@[simp]
theorem ContinuousLinearEquiv.coord_self (๐ : Type u_1) {E : Type u_2} [NormedField ๐] [NormedSpace ๐ E] (x : E) (h : x โ  0) :
() โจx, โฏโฉ = 1
noncomputable def LinearIsometryEquiv.toSpanUnitSingleton {๐ : Type u_1} {E : Type u_2} [] [Module ๐ E] [BoundedSMul ๐ E] (x : E) (hx : = 1) :
๐ โโแตข[๐] โฅ(Submodule.span ๐ {x})

Given a unit element x of a normed space E over a field ๐, the natural linear isometry equivalence from E to the span of x.

Equations
Instances For
@[simp]
theorem LinearIsometryEquiv.toSpanUnitSingleton_apply {๐ : Type u_1} {E : Type u_2} [] [Module ๐ E] [BoundedSMul ๐ E] (x : E) (hx : = 1) (r : ๐) :
= โจr โข x, โฏโฉ