linearEquiv — Mathlib

English

There exists a canonical linear equivalence between WithLp p V and V, i.e., WithLp p V is canonically isomorphic to V as a K-vector space.

Русский

Существует каноническое линейное эквивалентное отображение между WithLp p V и V, т.е. WithLp p V канонически изоморфно V как векторному пространству над K.

LaTeX

$$$$ WithLp(p,V) \cong_K V. $$$$

Lean4

/-- `WithLp.equiv` as a linear equivalence. -/
@[simps -fullyApplied]
protected def linearEquiv [Semiring K] [AddCommGroup V] [Module K V] : WithLp p V ≃ₗ[K] V
    where
  __ := WithLp.equiv _ _
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  toFun := WithLp.ofLp
  invFun := WithLp.toLp p

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