English
Definition of the canonical isomorphism between (ι → 𝕜) and E when ι is finite and E is a normed space.
Русский
Каноническое изоморфное отображение между пространствами ι → 𝕜 и E в случае конечного множества ι и нормированного пространства E.
LaTeX
$$$\\text{piRing}(ι) : ((ι \\to 𝕜) \\\\to_L[𝕜] E) \\\\cong_L[𝕜] (ι \\to E)$$$
Lean4
/-- Any finite-dimensional vector space over a locally compact field is proper.
We do not register this as an instance to avoid an instance loop when trying to prove the
properness of `𝕜`, and the search for `𝕜` as an unknown metavariable. Declare the instance
explicitly when needed. -/
theorem proper [FiniteDimensional 𝕜 E] : ProperSpace E :=
by
have : ProperSpace 𝕜 := .of_locallyCompactSpace 𝕜
set e := ContinuousLinearEquiv.ofFinrankEq (@finrank_fin_fun 𝕜 _ _ (finrank 𝕜 E)).symm
exact e.symm.antilipschitz.properSpace e.symm.continuous e.symm.surjective
