not_injective_dotProduct_right — Mathlib

English

Similarly, the map x ↦ dotProduct x a is not necessarily injective when viewing x as the left factor.

Русский

Аналогично, отображение x ↦ dotProduct x a может быть неинъективным при рассмотрении x слева.

LaTeX

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

Lean4

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

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