coe_ofLinearIsometry_symm — Mathlib

English

The inverse evaluation of the constructed linear isometry equals the given inverse linear map.

Русский

Оценка обратного отображения эквивалентна данному обратному линейному отображению.

LaTeX

$$coe_ofLinearIsometry_symm : ((ofLinearIsometry f g h₁ h₂).symm : E₂ → E) = (g : E₂ → E)$$

Lean4

@[simp]
theorem coe_ofLinearIsometry_symm (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₂).symm : E₂ → E) = (g : E₂ → E) :=
  rfl

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