coeFn_toContinuousLinearEquivOfContinuous

English

Definition of upgrading a bijective continuous linear map between Banach spaces to a continuous linear equivalence when the direct map is continuous.

Русский

Определение апгрейда биективного непрерывного линейного отображения между банаховыми пространствами до непрерывной линейной эквивалентности, когда прямая карта непрерывна.

LaTeX

$$$\\text{ContinuousLinearEquiv.ofBijective}(f,h_f) : E\\to F \\quad \\text{is a continuous linear equivalence}$$$

Lean4

@[simp]
theorem coeFn_toContinuousLinearEquivOfContinuous (e : E ≃ₛₗ[σ] F) (h : Continuous e) :
    ⇑(e.toContinuousLinearEquivOfContinuous h) = e :=
  rfl

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