Theorems · Theorem · geometry

InnerProductGeometry.angle_le_angle_add_angle

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

Triangle inequality for angles between vectors.

Defined in

Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpace