signedDist_linear_apply — Mathlib

English

The signed distance linear part equals the negation of the projection term in the appropriate decomposition.

Русский

Линейная часть подписанного расстояния равна противоположному члену проекции в разложении.

LaTeX

$$$$ (signedDist(v)).linear = \operatorname{inner}_V ( - \operatorname{normalize}(v), \cdot ). $$$$

Lean4

theorem signedDist_linear_apply : (signedDist v).linear w = .const ℝ P ⟪-normalize v, w⟫ :=
  rfl

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