toLinearIsometryEquiv_apply — Mathlib

English

For any x in E1, the value of the equivalence at x equals li(x): (li.toLinearIsometryEquiv h) x = li x.

Русский

Для любого x в E1 значение эквивалентности в точке x равно li(x): (li.toLinearIsometryEquiv h) x = li x.

LaTeX

$$$ (li.toLinearIsometryEquiv h) x = li x $$$

Lean4

@[simp]
theorem toLinearIsometryEquiv_apply (li : E₁ →ₗᵢ[R₁] F) (h : finrank R₁ E₁ = finrank R₁ F) (x : E₁) :
    (li.toLinearIsometryEquiv h) x = li x :=
  rfl

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