𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : ProperSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
e : E ≃L[𝕜] Fin (finrank 𝕜 E) → 𝕜 :=
  ContinuousLinearEquiv.ofFinrankEq (_ : finrank 𝕜 E = finrank 𝕜 (Fin (finrank 𝕜 E) → 𝕜))
⊢ ProperSpace E
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : ProperSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
⊢ ProperSpace E
set e := ContinuousLinearEquiv.ofFinrankEq (@finrank_fin_fun 𝕜 _ _ (finrank 𝕜 E)).symm
no goals
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : ProperSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
e : E ≃L[𝕜] Fin (finrank 𝕜 E) → 𝕜 :=
  ContinuousLinearEquiv.ofFinrankEq (_ : finrank 𝕜 E = finrank 𝕜 (Fin (finrank 𝕜 E) → 𝕜))
⊢ ProperSpace E
exact e.symm.antilipschitz.properSpace e.symm.continuous e.symm.surjective