innerSL_inj — Mathlib

English

The map x ↦ innerSL x is injective; equality of innerSL images implies equality of vectors.

Русский

Отображение x ↦ innerSL x инъективно; равенство изображений означает равенство векторов.

LaTeX

$$innerSL_inj: x = y ⇔ innerSL 𝕜 x = innerSL 𝕜 y$$

Lean4

@[simp]
theorem _root_.innerSL_inj {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} :
    innerSL 𝕜 x = innerSL 𝕜 y ↔ x = y :=
  (toDualMap 𝕜 E).injective.eq_iff

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