instCoeTCContinuousLinearMap — Mathlib

English

There is a canonical identification of LinearIsometryEquiv with Continuous Linear Equivalences via a coercion.

Русский

Существуют канонические переходы между LinearIsometryEquiv и ContinuousLinearEquiv с помощью приведения типов.

LaTeX

$$instance instCoeTCContinuousLinearEquiv : CoeTC (E \equiv_{\sigma} E') (E \equiv_{SL[\sigma]} E')$$

Lean4

instance instCoeTCContinuousLinearMap : CoeTC (E ≃ₛₗᵢ[σ₁₂] E₂) (E →SL[σ₁₂] E₂) :=
  ⟨fun e => ↑(e : E ≃SL[σ₁₂] E₂)⟩

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