toContinuousLinearMap — Mathlib

English

There is a canonical class of continuous linear maps from E to F' when E is finite-dimensional.

Русский

Существуют канонические классы непрерывных линейных отображений из E в F' при конечной размерности E.

LaTeX

$$$\\text{ContinuousLinearMapClass} (E \\to_{𝕜} F')$$$

Lean4

/-- The continuous linear map induced by a linear map on a finite-dimensional space -/
def toContinuousLinearMap : (E →ₗ[𝕜] F') ≃ₗ[𝕜] E →L[𝕜] F'
    where
  toFun f := ⟨f, f.continuous_of_finiteDimensional⟩
  invFun := (↑)
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  right_inv _ := ContinuousLinearMap.coe_injective rfl

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