signedDist_vadd_left — Mathlib

English

The left translation by w adds a constant to signedDist: signedDist v (w + p) q = -⟪normalize(v), w⟫ + signedDist v p q.

Русский

Левое приращение на w добавляет константу к signedDist: signedDist v (w + p) q = -⟪normalize(v), w⟫ + signedDist v p q.

LaTeX

$$signedDist v (w+ p) q = -\,⟨\operatorname{normalize}(v), w\rangle + signedDist v p q$$

Lean4

theorem signedDist_vadd_left : signedDist v (w +ᵥ p) q = -⟪normalize v, w⟫ + signedDist v p q := by
  simp [signedDist_linear_apply_apply]

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