Theorems · Theorem · geometry

InnerProductGeometry.angle_add_angle_eq_pi_of_angle_eq_pi

∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V} (z : V),
  InnerProductGeometry.angle x y = Real.pi → InnerProductGeometry.angle x z + InnerProductGeometry.angle y z = Real.pi

If the angle between two vectors is π, the angles between those vectors and a third vector add to π.

Defined in

Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpace