Theorems · Theorem · geometry

InnerProductGeometry.angle_eq_angle_add_add_angle_add_of_mem_span

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

The triangle inequality is an equality if the middle vector is a nonnegative linear combination of the other two vectors. See angle_add_angle_eq_pi_of_angle_eq_pi for the other equality case.

Defined in

Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpace