English
Let E1 and F be finite-dimensional normed spaces over a field R1, and let li: E1 →ₗᵢ[R₁] F be a linear isometry. If finrank R₁ E₁ = finrank R₁ F, then li can be upgraded to a linear isometry equivalence E₁ ≃ₗᵢ[R₁] F.
Русский
Пусть E1 и F — конечномерные нормированные пространства над полем R1, и пусть li: E1 →ₗᵢ[R₁] F — линейная изометрия. При условии finrank R₁ E₁ = finrank R₁ F можно перейти к линейной изометрической эквивалентности E₁ ≃ₗᵢ[R₁] F.
LaTeX
$$$\exists T: E_1 \simeq_{\mathrm{LI}} F,\ T = li^{\mathrm{toLinearIsometryEquiv}}(h).$$$
Lean4
/-- A linear isometry between finite-dimensional spaces of equal dimension can be upgraded
to a linear isometry equivalence. -/
def toLinearIsometryEquiv (li : E₁ →ₗᵢ[R₁] F) (h : finrank R₁ E₁ = finrank R₁ F) : E₁ ≃ₗᵢ[R₁] F
where
toLinearEquiv := li.toLinearMap.linearEquivOfInjective li.injective h
norm_map' := li.norm_map'
