English
If K is a locally compact complete normed field and V is a finite-dimensional vector space over K, then V is locally compact.
Русский
Если K — локально компактное поле, и V — конечномерное пространство над K, то V локально компактно.
LaTeX
$$LocallyCompactSpace(K) and FiniteDimensional(K,V) imply LocallyCompactSpace(V)$$
Lean4
/-- An injective linear map with finite-dimensional domain is a closed embedding. -/
theorem isClosedEmbedding_of_injective [T2Space E] [FiniteDimensional 𝕜 E] {f : E →ₗ[𝕜] F} (hf : LinearMap.ker f = ⊥) :
IsClosedEmbedding f :=
let g := LinearEquiv.ofInjective f (LinearMap.ker_eq_bot.mp hf)
{ IsEmbedding.subtypeVal.comp g.toContinuousLinearEquiv.toHomeomorph.isEmbedding with
isClosed_range := by
haveI := f.finiteDimensional_range
simpa [LinearMap.coe_range f] using (LinearMap.range f).closed_of_finiteDimensional }
