coe_toContinuousLinearMap — Mathlib

English

A linear equivalence between finite-dimensional spaces lifts to a continuous linear equivalence.

Русский

Линейное эквивалентное отображение между конечномерными пространствами можно превратить в непрерывное линейное эквивалентное отображение.

LaTeX

$$$\\text{lift } e : (E \\simeq_{𝕜} F) \\to (E \\overset{\\sim}{\\to} F)\\;\\text{continuous}$$$

Lean4

@[simp]
theorem coe_toContinuousLinearMap (f : E →ₗ[𝕜] F') : ((LinearMap.toContinuousLinearMap f) : E →ₗ[𝕜] F') = f :=
  rfl

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