# 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.

source
theorem LinearMap.toSpanSingleton_homothety (𝕜 : Type u_1) {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [NormSMulClass 𝕜 E] (x : E) (c : 𝕜) :
‖(toSpanSingleton 𝕜 E x) c‖ = ‖x‖ * ‖c‖
source
theorem LinearEquiv.toSpanNonzeroSingleton_homothety (𝕜 : Type u_1) {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [NormSMulClass 𝕜 E] (x : E) (h : x ≠ 0) (c : 𝕜) :
‖(toSpanNonzeroSingleton 𝕜 E x h) c‖ = ‖x‖ * ‖c‖
source
noncomputable def ContinuousLinearEquiv.toSpanNonzeroSingleton (𝕜 : Type u_1) {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [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 `𝕜` to the span of `x`.

Equations

- ContinuousLinearEquiv.toSpanNonzeroSingleton 𝕜 x h = ContinuousLinearEquiv.ofHomothety (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x h) ‖x‖ ⋯ ⋯

Instances For

source
@[simp]
theorem ContinuousLinearEquiv.toSpanNonzeroSingleton_apply_coe (𝕜 : Type u_1) {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (h : x ≠ 0) (a✝ : 𝕜) :
↑((toSpanNonzeroSingleton 𝕜 x h) a✝) = a✝ • x
source
@[simp]
theorem ContinuousLinearEquiv.toSpanNonzeroSingleton_symm_apply (𝕜 : Type u_1) {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (h : x ≠ 0) (a✝ : ↥(Submodule.span 𝕜 {x})) :
(toSpanNonzeroSingleton 𝕜 x h).symm a✝ = (LinearEquiv.ofInjective (LinearMap.toSpanSingleton 𝕜 E x) ⋯).symm ((LinearEquiv.ofEq (Submodule.span 𝕜 {x}) (LinearMap.range (LinearMap.toSpanSingleton 𝕜 E x)) ⋯) a✝)
source
noncomputable def ContinuousLinearEquiv.coord (𝕜 : Type u_1) {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (h : x ≠ 0) :
StrongDual 𝕜 ↥(Submodule.span 𝕜 {x})

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

- ContinuousLinearEquiv.coord 𝕜 x h = ↑(ContinuousLinearEquiv.toSpanNonzeroSingleton 𝕜 x h).symm

Instances For

source
@[simp]
theorem ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm (𝕜 : Type u_1) {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} (h : x ≠ 0) :
⇑(toSpanNonzeroSingleton 𝕜 x h).symm = ⇑(coord 𝕜 x h)
source
@[simp]
theorem ContinuousLinearEquiv.coord_toSpanNonzeroSingleton (𝕜 : Type u_1) {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} (h : x ≠ 0) (c : 𝕜) :
(coord 𝕜 x h) ((toSpanNonzeroSingleton 𝕜 x h) c) = c
source
@[simp]
theorem ContinuousLinearEquiv.toSpanNonzeroSingleton_coord (𝕜 : Type u_1) {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} (h : x ≠ 0) (y : ↥(Submodule.span 𝕜 {x})) :
(toSpanNonzeroSingleton 𝕜 x h) ((coord 𝕜 x h) y) = y
source
@[simp]
theorem ContinuousLinearEquiv.coord_self (𝕜 : Type u_1) {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (h : x ≠ 0) :
(coord 𝕜 x h) ⟨x, ⋯⟩ = 1
source
noncomputable def LinearIsometryEquiv.toSpanUnitSingleton {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [NormSMulClass 𝕜 E] (x : E) (hx : ‖x‖ = 1) :
𝕜 ≃ₗᵢ[𝕜] ↥(Submodule.span 𝕜 {x})

Given a unit element `x` of a normed space `E` over a field `𝕜`, the natural linear isometry equivalence from `𝕜` to the span of `x`.

Equations

- LinearIsometryEquiv.toSpanUnitSingleton x hx = { toLinearEquiv := LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem LinearIsometryEquiv.toSpanUnitSingleton_apply {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [NormSMulClass 𝕜 E] (x : E) (hx : ‖x‖ = 1) (r : 𝕜) :
(toSpanUnitSingleton x hx) r = ⟨r • x, ⋯⟩