Theorems · Theorem · geometry

dist_sq_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}, inner ℝ (p -ᵥ a) (b -ᵥ a) = 0 → dist p b ^ 2 = dist p a ^ 2 + dist a b ^ 2

Pythagorean theorem: if p -ᵥ a is orthogonal to b -ᵥ a, then dist p b ^ 2 = dist p a ^ 2 + dist a b ^ 2.

Defined in

Mathlib.Analysis.InnerProductSpace.Affine

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor