coe_toContinuousLinearEquiv_symm — Mathlib

English

There is a lifting from linear equivalences to continuous linear equivalences for finite-dimensional spaces.

Русский

Существует переход от линейных эквивалентностей к непрерывным линейным эквивалентностям для конечномерных пространств.

LaTeX

$$@[simp] CanLift (E ≃ₗ[𝕜] F) (E ≃L[𝕜] F) ContinuousLinearEquiv.toLinearEquiv fun _ => True$$

Lean4

@[simp]
theorem coe_toContinuousLinearEquiv_symm (e : E ≃ₗ[𝕜] F) : (e.toContinuousLinearEquiv.symm : F →ₗ[𝕜] E) = e.symm :=
  rfl

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