toLinearMap_eq_iff_eq_toContinuousLinearMap

English

The coercion from a linear map to its associated continuous linear map is the identity on the underlying function.

Русский

Приведение линейного отображения к соответствующему непрерывному линейному отображению идентично самой функции.

LaTeX

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

Lean4

theorem _root_.ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMap (g : E →L[𝕜] E) (f : E →ₗ[𝕜] E) :
    g.toLinearMap = f ↔ g = f.toContinuousLinearMap := by simp [ContinuousLinearMap.ext_iff, LinearMap.ext_iff]

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