toContinuousLinearEquivOfContinuous

English

If e: E ≃ₛₗ[σ] F and h is continuous, then the inverse of the constructed continuous linear equivalence has underlying function equal to the inverse of e.

Русский

Если e: E ≃ₛₗ[σ] F и h непрерывно, то обратное соответствие к созданной непрерывной линейной эквивалентности имеет основанную функцию равной обратному от e.

LaTeX

$$$\\bigl(e^{\\mathrm{cont}}\\bigr)^{-1} = e^{-1}$ as functions$$

Lean4

/-- Associating to a linear equivalence between Banach spaces a continuous linear equivalence when
the direct map is continuous, thanks to the Banach open mapping theorem that ensures that the
inverse map is also continuous. -/
def toContinuousLinearEquivOfContinuous (e : E ≃ₛₗ[σ] F) (h : Continuous e) : E ≃SL[σ] F :=
  { e with
    continuous_toFun := h
    continuous_invFun := e.continuous_symm h }

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