Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-03 17:40 6d5dda18

View on Github →

feat(geometry/euclidean/basic): angles and betweenness (#16734) Add some basic lemmas about the relation between (unoriented) angles and betweenness of points.

Estimated changes

Modified src/geometry/euclidean/basic.lean

added theorem euclidean_geometry.angle_eq_pi_iff_sbtw

added theorem euclidean_geometry.angle_eq_zero_iff_eq_and_ne_or_sbtw

added theorem euclidean_geometry.angle_eq_zero_iff_ne_and_wbtw

added theorem sbtw.angle₁₂₃_eq_pi

added theorem sbtw.angle₁₃₂_eq_zero

added theorem sbtw.angle₂₁₃_eq_zero

added theorem sbtw.angle₂₃₁_eq_zero

added theorem sbtw.angle₃₁₂_eq_zero

added theorem sbtw.angle₃₂₁_eq_pi

added theorem wbtw.angle₁₃₂_eq_zero_of_ne

added theorem wbtw.angle₂₁₃_eq_zero_of_ne

added theorem wbtw.angle₂₃₁_eq_zero_of_ne

added theorem wbtw.angle₃₁₂_eq_zero_of_ne