toContinuousLinearMap — Mathlib

English

Every endomorphism of a finite-dimensional space is associated with a continuous linear endomorphism.

Русский

Любой эндоморфизм конечномерного пространства соответствует непрерывному линейному эндоморфизму.

LaTeX

$$$\\forall f \\in \\mathrm{End}_{𝕜}(E),\\; f \\mapsto f \\;\\text{gives a } E \\to_L E$$$

Lean4

/-- Algebra equivalence between the linear maps and continuous linear maps on a finite-dimensional
space. -/
def _root_.Module.End.toContinuousLinearMap (E : Type v) [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    [FiniteDimensional 𝕜 E] : (E →ₗ[𝕜] E) ≃ₐ[𝕜] (E →L[𝕜] E) :=
  { LinearMap.toContinuousLinearMap with
    map_mul' := fun _ _ ↦ rfl
    commutes' := fun _ ↦ rfl }

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