instFiniteDimensionalContinuousLinearMapId

English

If E and F are finite-dimensional over a field 𝕜, then the space of continuous linear maps E →L𝕜 F is finite-dimensional.

Русский

Если пространства E и F над полем 𝕜 конечномерны, то пространство непрерывных линейных отображений E →L𝕜 F конечно-мерно.

LaTeX

$$$\text{FiniteDimensional}_{\mathbb{K}}(E) \land \text{FiniteDimensional}_{\mathbb{K}}(F) \Rightarrow \mathrm{FiniteDimensional}_{\mathbb{K}}(E \to_L[\mathbb{K}] F)$$$

Lean4

/-- The space of continuous linear maps between finite-dimensional spaces is finite-dimensional. -/
instance [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] : FiniteDimensional 𝕜 (E →L[𝕜] F) :=
  FiniteDimensional.of_injective (ContinuousLinearMap.coeLM 𝕜 : (E →L[𝕜] F) →ₗ[𝕜] E →ₗ[𝕜] F)
    ContinuousLinearMap.coe_injective

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