ofFinrankEq — Mathlib

English

If two finite-dimensional topological vector spaces E and F over a complete normed field 𝕜 satisfy finrank 𝕜 E = finrank 𝕜 F, then there exists a continuous linear equivalence E ≃L[𝕜] F.

Русский

Если два конечномерных топологических векторных пространства E и F над полем 𝕜 имеют равные конечные размерности, существует непрерывно линейное изоморфизм E ≃L[𝕜] F.

LaTeX

$$$\\operatorname{finrank}_{𝕜} E = \\operatorname{finrank}_{𝕜} F \\Rightarrow E \\simeq_L[𝕜] F$$$

Lean4

/-- A continuous linear equivalence between two finite-dimensional topological vector spaces over a
complete normed field of the same (finite) dimension. -/
def ofFinrankEq (cond : finrank 𝕜 E = finrank 𝕜 F) : E ≃L[𝕜] F :=
  (LinearEquiv.ofFinrankEq E F cond).toContinuousLinearEquiv

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