English
A finite-dimensional vector space over an RCLike field is a proper metric space.
Русский
Конечномерное векторное пространство над полем RCLike является правильным метрическим пространством.
LaTeX
$$$\\operatorname{FiniteDimensional}_{K} E \\Rightarrow \\operatorname{ProperSpace} E$$$
Lean4
/-- A finite-dimensional vector space over an `RCLike` is a proper metric space.
This is not an instance because it would cause a search for `FiniteDimensional ?x E` before
`RCLike ?x`. -/
theorem proper_rclike [FiniteDimensional K E] : ProperSpace E := by
-- Using `have` not `let` since it is only existence of `NormedSpace` structure that we need.
have : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E
have : FiniteDimensional ℝ E := FiniteDimensional.trans ℝ K E
infer_instance
