coe_ofLinearIsometry — Mathlib

English

The underlying function of the constructed linear isometry from a given linear isometry coincides with the original function.

Русский

Функция подлежащей линейной изометрии совпадает с исходной функцией.

LaTeX

$$coe_ofLinearIsometry : (ofLinearIsometry f g h₁ h₂ : E → E₂) = f$$

Lean4

@[simp]
theorem coe_ofLinearIsometry (f : E →ₛₗᵢ[σ₁₂] E₂) (g : E₂ →ₛₗ[σ₂₁] E) (h₁ : f.toLinearMap.comp g = LinearMap.id)
    (h₂ : g.comp f.toLinearMap = LinearMap.id) : (ofLinearIsometry f g h₁ h₂ : E → E₂) = (f : E → E₂) :=
  rfl

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