K : Type u_1
E : Type u_2
inst✝³ : IsROrC K
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace K E
inst✝ : FiniteDimensional K E
this : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E
⊢ ProperSpace E
K : Type u_1
E : Type u_2
inst✝³ : IsROrC K
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace K E
inst✝ : FiniteDimensional K E
⊢ ProperSpace E
letI : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E
K : Type u_1
E : Type u_2
inst✝³ : IsROrC K
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace K E
inst✝ : FiniteDimensional K E
this✝ : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E
this : FiniteDimensional ℝ E := trans ℝ K E
⊢ ProperSpace E
K : Type u_1
E : Type u_2
inst✝³ : IsROrC K
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace K E
inst✝ : FiniteDimensional K E
this : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E
⊢ ProperSpace E
letI : FiniteDimensional ℝ E := FiniteDimensional.trans ℝ K E
no goals
K : Type u_1
E : Type u_2
inst✝³ : IsROrC K
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace K E
inst✝ : FiniteDimensional K E
this✝ : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E
this : FiniteDimensional ℝ E := trans ℝ K E
⊢ ProperSpace E
infer_instance