toWeakSpace — Mathlib

English

There is a canonical linear equivalence between E and the weak space: E ≃𝕜 WeakSpace 𝕜 E.

Русский

Существует каноническое линейное эквивалентности между E и слабым пространством: E ≃𝕜 WeakSpace 𝕜 E.

LaTeX

$$$toWeakSpace : E \\simeq_{\\mathbb{K}} \\mathrm{WeakSpace} 𝕜 E$$$

Lean4

/-- There is a canonical map `E → WeakSpace 𝕜 E` (the "identity"
mapping). It is a linear equivalence. -/
def toWeakSpace : E ≃ₗ[𝕜] WeakSpace 𝕜 E :=
  LinearEquiv.refl 𝕜 E

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