English
A vector is determined by all its inner products with the vectors of a basis: if for every basis vector b_i we have ⟪b_i, x⟫ = ⟪b_i, y⟫, then x = y.
Русский
Вектор определяется по всем скалярным произведениям с базисными векторaми: если для каждого b_i выполнено ⟪b_i, x⟫ = ⟪b_i, y⟫, то x = y.
LaTeX
$$\forall i, \; \langle b_i, x \rangle = \langle b_i, y \rangle \Rightarrow x = y$$
Lean4
theorem ext_inner_left_basis {ι : Type*} {x y : E} (b : Basis ι 𝕜 E) (h : ∀ i : ι, ⟪b i, x⟫ = ⟪b i, y⟫) : x = y :=
by
apply (toDualMap 𝕜 E).map_eq_iff.mp
refine (Function.Injective.eq_iff ContinuousLinearMap.coe_injective).mp (b.ext ?_)
intro i
simp only [ContinuousLinearMap.coe_coe]
rw [toDualMap_apply, toDualMap_apply]
rw [← inner_conj_symm]
conv_rhs => rw [← inner_conj_symm]
exact congr_arg conj (h i)
