ofBijective — Mathlib

English

The function underlying the bijective linear equivalence coincides with the original linear map.

Русский

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

LaTeX

$$$(\\text{ofBijective } f hinj hsurj) = f$ as a function$$

Lean4

/-- Convert a bijective continuous linear map `f : E →SL[σ] F` from a Banach space to a normed space
to a continuous linear equivalence. -/
noncomputable def ofBijective (f : E →SL[σ] F) (hinj : ker f = ⊥) (hsurj : LinearMap.range f = ⊤) : E ≃SL[σ] F :=
  (LinearEquiv.ofBijective f
        ⟨LinearMap.ker_eq_bot.mp hinj, LinearMap.range_eq_top.mp hsurj⟩).toContinuousLinearEquivOfContinuous
    (by exact f.continuous)

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