signedDist_apply_linear — Mathlib

English

The linear part of the signed distance corresponds to the inner product with the normalized direction.

Русский

Линейная часть подписанного расстояния связана с inner-произведением по нормализованному направлению.

LaTeX

$$$$\operatorname{signedDist}(v)\text{ is linear in } w,\text{ with } (signedDist(v)).linear = \langle -\operatorname{normalize}(v), w\rangle.$$$$

Lean4

theorem signedDist_apply_linear : (signedDist v p).linear = innerₗ V (normalize v) :=
  by
  change (innerₗ V (normalize v)).comp (LinearMap.id - 0) = _
  simp

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