signedDist_smul — Mathlib

English

For any v ∈ V and p,q ∈ P, and any r ∈ ℝ, the signed distance satisfies signedDist (r v) p q = Sign(r) · signedDist v p q.

Русский

Для любого v ∈ V, p,q ∈ P и любого скаляра r ∈ ℝ выполняется signedDist (r v) p q = Sign(r) · signedDist v p q.

LaTeX

$$$signedDist(r\cdot v)\ p\ q = \operatorname{SignType.sign}(r) \cdot signedDist(v)\ p\ q$$$

Lean4

theorem signedDist_smul (r : ℝ) : signedDist (r • v) p q = SignType.sign r * signedDist v p q :=
  by
  simp only [signedDist_apply_apply]
  rw [normalize_smul, real_inner_smul_left]

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