continuousLinearMapClassOfFiniteDimensional

English

For a finite index set ι and a basis ξ of E, the coordinate map ξ.equivFun: E → ι → 𝕜 is continuous.

Русский

Для конечного множества индексов ι и базиса ξ пространства E координатное отображение ξ.equivFun: E → ι → 𝕜 непрерывно.

LaTeX

$$$\\xi : \\text{Basis}_{ι}(E) \\quad\\Rightarrow\\quad \\xi\\!\\equivFun : E \\to ι \\to 𝕜 \\text{ is continuous}$$$

Lean4

instance continuousLinearMapClassOfFiniteDimensional [T2Space E] [FiniteDimensional 𝕜 E] :
    ContinuousLinearMapClass (E →ₗ[𝕜] F') 𝕜 E F' :=
  { LinearMap.semilinearMapClass with map_continuous := fun f => f.continuous_of_finiteDimensional }

Похожие утверждения