Theorems · Theorem · geometry

InnerProductGeometry.angle_eq_angle_add_angle_iff

∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y z : V},
  y ≠ 0 →
    (InnerProductGeometry.angle x z = InnerProductGeometry.angle x y + InnerProductGeometry.angle y z ↔
      InnerProductGeometry.angle x z = Real.pi ∨ y ∈ Submodule.span NNReal {x, z})

The triangle inequality on vectors x, y, z is an equality if and only if angle x z = π, or y is a nonnegative linear combination of x and z.

Defined in

Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpace