mkContinuousOfExistsBound_coe — Mathlib

English

The constructed continuous linear map from mkContinuous agrees with the original linear map on the underlying functions.

Русский

Сохранение совпадения функций при переходе к непрерывному отображению.

LaTeX

$$$(f.mkContinuous h).toLinearMap = f$$$

Lean4

@[simp, norm_cast]
theorem mkContinuousOfExistsBound_coe (h : ∃ C, ∀ x, ‖f x‖ ≤ C * ‖x‖) :
    (f.mkContinuousOfExistsBound h : E →ₛₗ[σ] F) = f :=
  rfl

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