coe_toContinuousLinearMap' — Mathlib

English

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

Русский

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

LaTeX

$$$\\text{coe to CM} : (E \\to_{𝕜} F') \\mapsto (E \\to_L 𝕜 F')$ with coe = id on functions$$

Lean4

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

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