English
In finite dimensions, the coordinate identification with a product space is continuous.
Русский
В конечномерном случае координатная идентификация с произведением пространств непрерывна.
LaTeX
$$$\\text{Continuous}(\\xi.\\equivFun)$$$
Lean4
/-- In finite dimensions over a non-discrete complete normed field, the canonical identification
(in terms of a basis) with `𝕜^n` (endowed with the product topology) is continuous.
This is the key fact which makes all linear maps from a T2 finite-dimensional TVS over such a field
continuous (see `LinearMap.continuous_of_finiteDimensional`), which in turn implies that all
norms are equivalent in finite dimensions. -/
theorem continuous_equivFun_basis [T2Space E] {ι : Type*} [Finite ι] (ξ : Basis ι 𝕜 E) : Continuous ξ.equivFun :=
haveI : FiniteDimensional 𝕜 E := .of_fintype_basis ξ
ξ.equivFun.toLinearMap.continuous_of_finiteDimensional
