ofBijective_symm_apply_apply — Mathlib

English

If a bounded linear bijection between normed spaces is continuous, then its inverse is continuous.

Русский

Если ограниченное линейное биективное отображение между нормированными пространствами непрерывно, то его обратное отображение непрерывно.

LaTeX

$$$\\text{continuous\_symm}(e,h):\\; E \\overset{e}{\\to} F \\Rightarrow E \\gets F$ непрерывно$$

Lean4

@[simp]
theorem ofBijective_symm_apply_apply (f : E →SL[σ] F) (hinj : ker f = ⊥) (hsurj : LinearMap.range f = ⊤) (x : E) :
    (ofBijective f hinj hsurj).symm (f x) = x :=
  (ofBijective f hinj hsurj).symm_apply_apply x

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