Theorems · Theorem · geometry

dist_sq_lineMap_of_inner_eq_zero

∀ {V : Type u_2} {P : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b p : P} (t : ℝ),
  inner ℝ (p -ᵥ a) (b -ᵥ a) = 0 → dist p ((AffineMap.lineMap a b) t) ^ 2 = dist p a ^ 2 + t ^ 2 * dist a b ^ 2

Squared distance from p to a point on the line from a to b, given that p -ᵥ a is orthogonal to b -ᵥ a.

Defined in

Mathlib.Analysis.InnerProductSpace.Affine

Cited by

3 results in Mathlib

Foundations

Depth 165 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor