nonempty_continuousLinearEquiv_of_finrank_eq

English

The canonical rearrangement of nested products coincides with the standard product rearrangement; the underlying maps agree with the standard Equiv.prodProdProdComm.

Русский

Каноническое переставление вложенных произведений совпадает со стандартным переставлением; соответствующие отображения совпадают со стандартной Equiv.prodProdProdComm.

LaTeX

$$$\\text{the underlying map equals } Equiv.prodProdProdComm(M_1,M_2,M_3,M_4)$$$

Lean4

/-- Two finite-dimensional topological vector spaces over a complete normed field are continuously
linearly equivalent if they have the same (finite) dimension. -/
theorem nonempty_continuousLinearEquiv_of_finrank_eq (cond : finrank 𝕜 E = finrank 𝕜 F) : Nonempty (E ≃L[𝕜] F) :=
  (nonempty_linearEquiv_of_finrank_eq cond).map LinearEquiv.toContinuousLinearEquiv

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