The Triangle Inequality for Angles

This file contains the proof that angles obey the triangle inequality.

theorem InnerProductGeometry.angle_le_angle_add_angle {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x y z : V) : angle x z ≤ angle x y + angle y z

Triangle inequality for angles between vectors.

theorem InnerProductGeometry.angle_eq_angle_add_add_angle_add_of_mem_span {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y z : V} (hy : y ≠ 0) (h_mem : y ∈ Submodule.span NNReal {x, z}) : angle x z = angle x y + 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.

theorem InnerProductGeometry.angle_eq_angle_add_angle_iff {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y z : V} (hy : y ≠ 0) : angle x z = angle x y + angle y z ↔ 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.

theorem EuclideanGeometry.angle_le_angle_add_angle {V : Type u_2} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p p₁ p₂ p₃ : P) : angle p₁ p p₃ ≤ angle p₁ p p₂ + angle p₂ p p₃

Triangle inequality for angles in Euclidean geometry.