not_injective_dotProduct_left — Mathlib

English

For a fixed vector a, the map x ↦ dotProduct x a is not necessarily injective; in particular, there exist distinct x with the same dotProduct.

Русский

Для фиксированного вектора a отображение x ↦ dotProduct x a не обязательно инъективно; существуют различные x, дающие одинаковый dotProduct.

LaTeX

$$$ \neg \operatorname{Injective}( \lambda x, \ dotProduct(x,a) ) $$$

Lean4

theorem not_injective_dotProduct_left (a : m → α) : ¬Function.Injective (dotProduct a) :=
  by
  intro h
  obtain ⟨b, hb, hba⟩ := exists_ne_zero_dotProduct_eq_zero a
  simpa [dotProduct_comm a b, hba, hb] using @h b 0

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