reflection_singleton_apply — Mathlib

English

Reflection in the one-dimensional subspace spanned by a nonzero vector u sends any v to the standard reflection about the line through u, namely twice the projection of v onto u minus v.

Русский

Отражение в одномерном подпоставном пространстве, порождённом ненулевым вектором u, отправляет v в v, отражённое по прямой через u:

LaTeX

$$$\mathrm{Ref}_{\operatorname{span}(u)}(v) = 2\,\frac{\langle u,v\rangle}{\|u\|^2}\,u - v$$$

Lean4

theorem reflection_singleton_apply (u v : E) : reflection (𝕜 ∙ u) v = 2 • (⟪u, v⟫ / ((‖u‖ : 𝕜) ^ 2)) • u - v := by
  rw [reflection_apply, starProjection_singleton, ofReal_pow]

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