English
Let E and F be finite-dimensional topological vector spaces over a complete normed field 𝕜. There exists a continuous linear isomorphism E ≃L[𝕜] F if and only if their finite dimensions agree, i.e. finrank 𝕜 E = finrank 𝕜 F.
Русский
Пусть E и F — конечномерные топологические векторные пространства над полем 𝕜, являющимся полем с нормой. Существуют непрерывно линейные эквивалентности E ≃L[𝕜] F тогда и только тогда, когда их конечные размерности равны: finrank 𝕜 E = finrank 𝕜 F.
LaTeX
$$$\\exists \\phi: E \\simeq_L[\\,𝕜\\] F \\quad \\Longleftrightarrow\\quad \\operatorname{finrank}_{𝕜} E = \\operatorname{finrank}_{𝕜} F$$$
Lean4
/-- Two finite-dimensional topological vector spaces over a complete normed field are continuously
linearly equivalent if and only if they have the same (finite) dimension. -/
theorem nonempty_continuousLinearEquiv_iff_finrank_eq : Nonempty (E ≃L[𝕜] F) ↔ finrank 𝕜 E = finrank 𝕜 F :=
⟨fun ⟨h⟩ => h.toLinearEquiv.finrank_eq, fun h => FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq h⟩
