ext_inner_right_basis — Mathlib

English

A vector is determined by its inner products with the basis vectors on the right: if ⟪x, b_i⟫ = ⟪y, b_i⟫ for all i, then x = y.

Русский

Вектор определяется по всем скалярным произведениям с базисными векторами справа: если ⟪x, b_i⟫ = ⟪y, b_i⟫ для всех i, то x = y.

LaTeX

$$\forall i, \; \langle x, b_i \rangle = \langle y, b_i \rangle \Rightarrow x = y$$

Lean4

theorem ext_inner_right_basis {ι : Type*} {x y : E} (b : Basis ι 𝕜 E) (h : ∀ i : ι, ⟪x, b i⟫ = ⟪y, b i⟫) : x = y :=
  by
  refine ext_inner_left_basis b fun i => ?_
  rw [← inner_conj_symm]
  conv_rhs => rw [← inner_conj_symm]
  exact congr_arg conj (h i)

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