clmOfExistsBoundedImage_coe — Mathlib

English

The underlying linear map of the constructed continuous linear map equals the original f.

Русский

Базовая линейная карта сконструированного непрерывного линейного отображения совпадает с исходным f.

LaTeX

$$$(f.clmOfExistsBoundedImage h : E \\to F) = f$$$

Lean4

theorem clmOfExistsBoundedImage_coe {f : E →ₗ[𝕜] F} {h : ∃ V ∈ 𝓝 (0 : E), Bornology.IsVonNBounded 𝕜 (f '' V)} :
    (f.clmOfExistsBoundedImage h : E →ₗ[𝕜] F) = f :=
  rfl

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