signedDist_linear_apply_apply — Mathlib

English

Let v,w ∈ V and p ∈ P. The linear part of the signed distance map in the p-variable, in the direction given by w, is the real number ⟪-normalize(v), w⟫; equivalently, (signedDist v).linear w p = ⟪-normalize(v), w⟫ for all p.

Русский

Пусть v,w ∈ V и p ∈ P. Линейная часть отображения signedDist(v) по переменной p в направлении w равна ⟪-normalize(v), w⟫; то есть (signedDist v).linear w p = ⟪-normalize(v), w⟫ для всех p.

LaTeX

$$$(signedDist\ v).linear w p = \langle -\operatorname{normalize}(v), w \rangle$$$

Lean4

theorem signedDist_linear_apply_apply : (signedDist v).linear w p = ⟪-normalize v, w⟫ :=
  rfl

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