Oriented angles. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines oriented angles in Euclidean affine spaces.
Main definitions #
euclidean_geometry.oangle, with notation∡, is the oriented angle determined by three points.
The oriented angle at p₂ between the line segments to p₁ and p₃, modulo 2 * π. If
either of those points equals p₂, this is 0. See euclidean_geometry.angle for the
corresponding unoriented angle definition.
Equations
- euclidean_geometry.oangle p₁ p₂ p₃ = module.oriented.positive_orientation.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
Oriented angles are continuous when neither end point equals the middle point.
The angle ∡AAB at a point.
The angle ∡ABB at a point.
The angle ∡ABA at a point.
If the angle between three points is nonzero, the first two points are not equal.
If the angle between three points is nonzero, the last two points are not equal.
If the angle between three points is nonzero, the first and third points are not equal.
If the angle between three points is π, the first two points are not equal.
If the angle between three points is π, the last two points are not equal.
If the angle between three points is π, the first and third points are not equal.
If the angle between three points is π / 2, the first two points are not equal.
If the angle between three points is π / 2, the last two points are not equal.
If the angle between three points is π / 2, the first and third points are not equal.
If the angle between three points is -π / 2, the first two points are not equal.
If the angle between three points is -π / 2, the last two points are not equal.
If the angle between three points is -π / 2, the first and third points are not equal.
If the sign of the angle between three points is nonzero, the first two points are not equal.
If the sign of the angle between three points is nonzero, the last two points are not equal.
If the sign of the angle between three points is nonzero, the first and third points are not equal.
If the sign of the angle between three points is positive, the first two points are not equal.
If the sign of the angle between three points is positive, the last two points are not equal.
If the sign of the angle between three points is positive, the first and third points are not equal.
If the sign of the angle between three points is negative, the first two points are not equal.
If the sign of the angle between three points is negative, the last two points are not equal.
If the sign of the angle between three points is negative, the first and third points are not equal.
Reversing the order of the points passed to oangle negates the angle.
Adding an angle to that with the order of the points reversed results in 0.
An oriented angle is zero if and only if the angle with the order of the points reversed is zero.
An oriented angle is π if and only if the angle with the order of the points reversed is
π.
An oriented angle is not zero or π if and only if the three points are affinely
independent.
An oriented angle is zero or π if and only if the three points are collinear.
If twice the oriented angles between two triples of points are equal, one triple is affinely independent if and only if the other is.
If twice the oriented angles between two triples of points are equal, one triple is collinear if and only if the other is.
If corresponding pairs of points in two angles have the same vector span, twice those angles are equal.
If the lines determined by corresponding pairs of points in two angles are parallel, twice those angles are equal.
Given three points not equal to p, the angle between the first and the second at p plus
the angle between the second and the third equals the angle between the first and the third.
Given three points not equal to p, the angle between the second and the third at p plus
the angle between the first and the second equals the angle between the first and the third.
Given three points not equal to p, the angle between the first and the third at p minus
the angle between the first and the second equals the angle between the second and the third.
Given three points not equal to p, the angle between the first and the third at p minus
the angle between the second and the third equals the angle between the first and the second.
Given three points not equal to p, adding the angles between them at p in cyclic order
results in 0.
Pons asinorum, oriented angle-at-point form.
The angle at the apex of an isosceles triangle is π minus twice a base angle, oriented
angle-at-point form.
A base angle of an isosceles triangle is acute, oriented angle-at-point form.
A base angle of an isosceles triangle is acute, oriented angle-at-point form.
The cosine of the oriented angle at p between two points not equal to p equals that of the
unoriented angle.
The oriented angle at p between two points not equal to p is plus or minus the unoriented
angle.
The unoriented angle at p between two points not equal to p is the absolute value of the
oriented angle.
If the sign of the oriented angle at p between two points is zero, either one of the points
equals p or the unoriented angle is 0 or π.
If two unoriented angles are equal, and the signs of the corresponding oriented angles are equal, then the oriented angles are equal (even in degenerate cases).
If the signs of two nondegenerate oriented angles between points are equal, the oriented angles are equal if and only if the unoriented angles are equal.
The oriented angle between three points equals the unoriented angle if the sign is positive.
The oriented angle between three points equals minus the unoriented angle if the sign is negative.
The unoriented angle at p between two points not equal to p is zero if and only if the
unoriented angle is zero.
The oriented angle between three points is π if and only if the unoriented angle is π.
If the oriented angle between three points is π / 2, so is the unoriented angle.
If the oriented angle between three points is π / 2, so is the unoriented angle
(reversed).
If the oriented angle between three points is -π / 2, the unoriented angle is π / 2.
If the oriented angle between three points is -π / 2, the unoriented angle (reversed) is
π / 2.
Swapping the first and second points in an oriented angle negates the sign of that angle.
Swapping the first and third points in an oriented angle negates the sign of that angle.
Swapping the second and third points in an oriented angle negates the sign of that angle.
Rotating the points in an oriented angle does not change the sign of that angle.
The oriented angle between three points is π if and only if the second point is strictly between the other two.
If the second of three points is strictly between the other two, the oriented angle at that point is π.
If the second of three points is strictly between the other two, the oriented angle at that point (reversed) is π.
If the second of three points is weakly between the other two, the oriented angle at the first point is zero.
If the second of three points is strictly between the other two, the oriented angle at the first point is zero.
If the second of three points is weakly between the other two, the oriented angle at the first point (reversed) is zero.
If the second of three points is strictly between the other two, the oriented angle at the first point (reversed) is zero.
If the second of three points is weakly between the other two, the oriented angle at the third point is zero.
If the second of three points is strictly between the other two, the oriented angle at the third point is zero.
If the second of three points is weakly between the other two, the oriented angle at the third point (reversed) is zero.
If the second of three points is strictly between the other two, the oriented angle at the third point (reversed) is zero.
The oriented angle between three points is zero if and only if one of the first and third points is weakly between the other two.
An oriented angle is unchanged by replacing the first point by one weakly further away on the same ray.
An oriented angle is unchanged by replacing the first point by one strictly further away on the same ray.
An oriented angle is unchanged by replacing the third point by one weakly further away on the same ray.
An oriented angle is unchanged by replacing the third point by one strictly further away on the same ray.
An oriented angle is unchanged by replacing the first point with the midpoint of the segment between it and the second point.
An oriented angle is unchanged by replacing the first point with the midpoint of the segment between the second point and that point.
An oriented angle is unchanged by replacing the third point with the midpoint of the segment between it and the second point.
An oriented angle is unchanged by replacing the third point with the midpoint of the segment between the second point and that point.
Replacing the first point by one on the same line but the opposite ray adds π to the oriented angle.
Replacing the third point by one on the same line but the opposite ray adds π to the oriented angle.
Replacing both the first and third points by ones on the same lines but the opposite rays does not change the oriented angle (vertically opposite angles).
Replacing the first point by one on the same line does not change twice the oriented angle.
Replacing the third point by one on the same line does not change twice the oriented angle.
Two different points are equidistant from a third point if and only if that third point
equals some multiple of a π / 2 rotation of the vector between those points, plus the midpoint
of those points.
Given two pairs of distinct points on the same line, such that the vectors between those pairs of points are on the same ray (oriented in the same direction on that line), and a fifth point, the angles at the fifth point between each of those two pairs of points have the same sign.
Given three points in strict order on the same line, and a fourth point, the angles at the fourth point between the first and second or second and third points have the same sign.
Given three points in weak order on the same line, with the first not equal to the second, and a fourth point, the angles at the fourth point between the first and second or first and third points have the same sign.
Given three points in strict order on the same line, and a fourth point, the angles at the fourth point between the first and second or first and third points have the same sign.
Given three points in weak order on the same line, with the second not equal to the third, and a fourth point, the angles at the fourth point between the second and third or first and third points have the same sign.
Given three points in strict order on the same line, and a fourth point, the angles at the fourth point between the second and third or first and third points have the same sign.
Given two points in an affine subspace, the angles between those two points at two other points on the same side of that subspace have the same sign.
Given two points in an affine subspace, the angles between those two points at two other points on opposite sides of that subspace have opposite signs.