coe_ofBijective — Mathlib

English

The symmetry of the constructed continuous linear equivalence preserves the underlying function via the inverse.

Русский

Симметрия созданной непрерывной линейной эквивалентности сохраняет исходную функцию через обратное отображение.

LaTeX

$$$\\bigl( e.toContinuousLinearEquivOfContinuous h \\bigr)^{-1} = e^{-1}$$$

Lean4

theorem coe_ofBijective (f : E →SL[σ] F) (hinj : ker f = ⊥) (hsurj : LinearMap.range f = ⊤) :
    ↑(ofBijective f hinj hsurj) = f := by
  ext
  rfl

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