Documentation

Mathlib.Analysis.Normed.Module.Span

The span of a single vector #

The equivalence of ๐•œ and ๐•œ โ€ข x for x โ‰  0 are defined as continuous linear equivalence and isometry.

Main definitions #

theorem LinearMap.toSpanSingleton_homothety (๐•œ : Type u_1) {E : Type u_2} [NormedDivisionRing ๐•œ] [SeminormedAddCommGroup E] [Module ๐•œ E] [BoundedSMul ๐•œ E] (x : E) (c : ๐•œ) :
theorem LinearEquiv.toSpanNonzeroSingleton_homothety (๐•œ : Type u_1) {E : Type u_2} [NormedDivisionRing ๐•œ] [SeminormedAddCommGroup E] [Module ๐•œ E] [BoundedSMul ๐•œ E] (x : E) (h : x โ‰  0) (c : ๐•œ) :
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 Eโ‚ to the span of x.

Equations
Instances For
    noncomputable def ContinuousLinearEquiv.coord (๐•œ : Type u_1) {E : Type u_2} [NormedField ๐•œ] [NormedAddCommGroup E] [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
    Instances For
      @[simp]
      theorem ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm (๐•œ : Type u_1) {E : Type u_2} [NormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} (h : x โ‰  0) :
      โ‡‘(ContinuousLinearEquiv.toSpanNonzeroSingleton ๐•œ x h).symm = โ‡‘(ContinuousLinearEquiv.coord ๐•œ x h)
      @[simp]
      theorem ContinuousLinearEquiv.coord_toSpanNonzeroSingleton (๐•œ : Type u_1) {E : Type u_2} [NormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} (h : x โ‰  0) (c : ๐•œ) :
      @[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})) :
      @[simp]
      theorem ContinuousLinearEquiv.coord_self (๐•œ : Type u_1) {E : Type u_2} [NormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] (x : E) (h : x โ‰  0) :
      (ContinuousLinearEquiv.coord ๐•œ x h) โŸจx, โ‹ฏโŸฉ = 1
      noncomputable def LinearIsometryEquiv.toSpanUnitSingleton {๐•œ : Type u_1} {E : Type u_2} [NormedDivisionRing ๐•œ] [SeminormedAddCommGroup E] [Module ๐•œ E] [BoundedSMul ๐•œ 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 E to the span of x.

      Equations
      Instances For
        @[simp]
        theorem LinearIsometryEquiv.toSpanUnitSingleton_apply {๐•œ : Type u_1} {E : Type u_2} [NormedDivisionRing ๐•œ] [SeminormedAddCommGroup E] [Module ๐•œ E] [BoundedSMul ๐•œ E] (x : E) (hx : โ€–xโ€– = 1) (r : ๐•œ) :
        (LinearIsometryEquiv.toSpanUnitSingleton x hx) r = โŸจr โ€ข x, โ‹ฏโŸฉ