English
If e: E ≃ₛₗ[σ] F is a bijection and e is continuous, then there exists a corresponding continuous linear equivalence ẽ: E ≃SL[σ] F.
Русский
Если e: E ≃ₛₗ[σ] F является биекция и непрерывна, то существует соответствующее непрерывное линейное эквивалентное отображение ẽ: E ≃SL[σ] F.
LaTeX
$$$\\exists ẽ: E \\to\\! F,\\; ẽ \\text{ непрерывна и } ẽ\\text{ является непрерывной линейной эквивалентностью}$$$
Lean4
/-- If a bounded linear map is a bijection, then its inverse is also a bounded linear map. -/
@[continuity]
theorem continuous_symm (e : E ≃ₛₗ[σ] F) (h : Continuous e) : Continuous e.symm :=
by
rw [continuous_def]
intro s hs
rw [← e.image_eq_preimage]
rw [← e.coe_coe] at h ⊢
exact ContinuousLinearMap.isOpenMap (σ := σ) ⟨_, h⟩ e.surjective s hs
