# mathlibdocumentation

geometry.euclidean.angle.oriented.affine

# Oriented angles. #

This file defines oriented angles in Euclidean affine spaces.

## Main definitions #

• `euclidean_geometry.oangle`, with notation `∡`, is the oriented angle determined by three points.
noncomputable def euclidean_geometry.oangle {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] (p₁ p₂ p₃ : P) :

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
• p₃ = (p₃ -ᵥ p₂)
theorem euclidean_geometry.continuous_at_oangle {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {x : P × P × P} (hx12 : x.fst x.snd.fst) (hx32 : x.snd.snd x.snd.fst) :
continuous_at (λ (y : P × P × P), y.snd.snd) x

Oriented angles are continuous when neither end point equals the middle point.

@[simp]
theorem euclidean_geometry.oangle_self_left {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] (p₁ p₂ : P) :
p₂ = 0

The angle ∡AAB at a point.

@[simp]
theorem euclidean_geometry.oangle_self_right {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] (p₁ p₂ : P) :
p₂ = 0

The angle ∡ABB at a point.

@[simp]
theorem euclidean_geometry.oangle_self_left_right {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] (p₁ p₂ : P) :
p₁ = 0

The angle ∡ABA at a point.

theorem euclidean_geometry.left_ne_of_oangle_ne_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ 0) :
p₁ p₂

If the angle between three points is nonzero, the first two points are not equal.

theorem euclidean_geometry.right_ne_of_oangle_ne_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ 0) :
p₃ p₂

If the angle between three points is nonzero, the last two points are not equal.

theorem euclidean_geometry.left_ne_right_of_oangle_ne_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ 0) :
p₁ p₃

If the angle between three points is nonzero, the first and third points are not equal.

theorem euclidean_geometry.left_ne_of_oangle_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = real.pi) :
p₁ p₂

If the angle between three points is `π`, the first two points are not equal.

theorem euclidean_geometry.right_ne_of_oangle_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = real.pi) :
p₃ p₂

If the angle between three points is `π`, the last two points are not equal.

theorem euclidean_geometry.left_ne_right_of_oangle_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = real.pi) :
p₁ p₃

If the angle between three points is `π`, the first and third points are not equal.

theorem euclidean_geometry.left_ne_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₁ p₂

If the angle between three points is `π / 2`, the first two points are not equal.

theorem euclidean_geometry.right_ne_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₃ p₂

If the angle between three points is `π / 2`, the last two points are not equal.

theorem euclidean_geometry.left_ne_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₁ p₃

If the angle between three points is `π / 2`, the first and third points are not equal.

theorem euclidean_geometry.left_ne_of_oangle_eq_neg_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (-real.pi / 2)) :
p₁ p₂

If the angle between three points is `-π / 2`, the first two points are not equal.

theorem euclidean_geometry.right_ne_of_oangle_eq_neg_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (-real.pi / 2)) :
p₃ p₂

If the angle between three points is `-π / 2`, the last two points are not equal.

theorem euclidean_geometry.left_ne_right_of_oangle_eq_neg_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (-real.pi / 2)) :
p₁ p₃

If the angle between three points is `-π / 2`, the first and third points are not equal.

theorem euclidean_geometry.left_ne_of_oangle_sign_ne_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃).sign 0) :
p₁ p₂

If the sign of the angle between three points is nonzero, the first two points are not equal.

theorem euclidean_geometry.right_ne_of_oangle_sign_ne_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃).sign 0) :
p₃ p₂

If the sign of the angle between three points is nonzero, the last two points are not equal.

theorem euclidean_geometry.left_ne_right_of_oangle_sign_ne_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃).sign 0) :
p₁ p₃

If the sign of the angle between three points is nonzero, the first and third points are not equal.

theorem euclidean_geometry.left_ne_of_oangle_sign_eq_one {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃).sign = 1) :
p₁ p₂

If the sign of the angle between three points is positive, the first two points are not equal.

theorem euclidean_geometry.right_ne_of_oangle_sign_eq_one {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃).sign = 1) :
p₃ p₂

If the sign of the angle between three points is positive, the last two points are not equal.

theorem euclidean_geometry.left_ne_right_of_oangle_sign_eq_one {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃).sign = 1) :
p₁ p₃

If the sign of the angle between three points is positive, the first and third points are not equal.

theorem euclidean_geometry.left_ne_of_oangle_sign_eq_neg_one {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃).sign = -1) :
p₁ p₂

If the sign of the angle between three points is negative, the first two points are not equal.

theorem euclidean_geometry.right_ne_of_oangle_sign_eq_neg_one {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃).sign = -1) :
p₃ p₂

If the sign of the angle between three points is negative, the last two points are not equal.

theorem euclidean_geometry.left_ne_right_of_oangle_sign_eq_neg_one {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃).sign = -1) :
p₁ p₃

If the sign of the angle between three points is negative, the first and third points are not equal.

theorem euclidean_geometry.oangle_rev {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] (p₁ p₂ p₃ : P) :
p₁ = - p₃

Reversing the order of the points passed to `oangle` negates the angle.

@[simp]
theorem euclidean_geometry.oangle_add_oangle_rev {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] (p₁ p₂ p₃ : P) :
p₃ + p₁ = 0

Adding an angle to that with the order of the points reversed results in 0.

theorem euclidean_geometry.oangle_eq_zero_iff_oangle_rev_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} :
p₃ = 0 p₁ = 0

An oriented angle is zero if and only if the angle with the order of the points reversed is zero.

theorem euclidean_geometry.oangle_eq_pi_iff_oangle_rev_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} :

An oriented angle is `π` if and only if the angle with the order of the points reversed is `π`.

theorem euclidean_geometry.oangle_ne_zero_and_ne_pi_iff_affine_independent {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} :
p₃ 0 p₃ real.pi ![p₁, p₂, p₃]

An oriented angle is not zero or `π` if and only if the three points are affinely independent.

theorem euclidean_geometry.oangle_eq_zero_or_eq_pi_iff_collinear {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} :
p₃ = 0 p₃ = real.pi {p₁, p₂, p₃}

An oriented angle is zero or `π` if and only if the three points are collinear.

theorem euclidean_geometry.affine_independent_iff_of_two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P} (h : 2 p₃ = 2 p₆) :
![p₁, p₂, p₃] ![p₄, p₅, p₆]

If twice the oriented angles between two triples of points are equal, one triple is affinely independent if and only if the other is.

theorem euclidean_geometry.collinear_iff_of_two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P} (h : 2 p₃ = 2 p₆) :
{p₁, p₂, p₃} {p₄, p₅, p₆}

If twice the oriented angles between two triples of points are equal, one triple is collinear if and only if the other is.

theorem euclidean_geometry.two_zsmul_oangle_of_vector_span_eq {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P} (h₁₂₄₅ : {p₁, p₂} = {p₄, p₅}) (h₃₂₆₅ : {p₃, p₂} = {p₆, p₅}) :
2 p₃ = 2 p₆

If corresponding pairs of points in two angles have the same vector span, twice those angles are equal.

theorem euclidean_geometry.two_zsmul_oangle_of_parallel {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P} (h₁₂₄₅ : {p₁, p₂}).parallel {p₄, p₅})) (h₃₂₆₅ : {p₃, p₂}).parallel {p₆, p₅})) :
2 p₃ = 2 p₆

If the lines determined by corresponding pairs of points in two angles are parallel, twice those angles are equal.

@[simp]
theorem euclidean_geometry.oangle_add {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p p₁ p₂ p₃ : P} (hp₁ : p₁ p) (hp₂ : p₂ p) (hp₃ : p₃ p) :
p₂ + p₃ = p₃

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.

@[simp]
theorem euclidean_geometry.oangle_add_swap {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p p₁ p₂ p₃ : P} (hp₁ : p₁ p) (hp₂ : p₂ p) (hp₃ : p₃ p) :
p₃ + p₂ = p₃

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.

@[simp]
theorem euclidean_geometry.oangle_sub_left {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p p₁ p₂ p₃ : P} (hp₁ : p₁ p) (hp₂ : p₂ p) (hp₃ : p₃ p) :
p₃ - p₂ = p₃

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.

@[simp]
theorem euclidean_geometry.oangle_sub_right {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p p₁ p₂ p₃ : P} (hp₁ : p₁ p) (hp₂ : p₂ p) (hp₃ : p₃ p) :
p₃ - p₃ = p₂

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.

@[simp]
theorem euclidean_geometry.oangle_add_cyc3 {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p p₁ p₂ p₃ : P} (hp₁ : p₁ p) (hp₂ : p₂ p) (hp₃ : p₃ p) :
p₂ + p₃ + p₁ = 0

Given three points not equal to `p`, adding the angles between them at `p` in cyclic order results in 0.

theorem euclidean_geometry.oangle_eq_oangle_of_dist_eq {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₂ = p₃) :
p₃ = p₁

Pons asinorum, oriented angle-at-point form.

theorem euclidean_geometry.oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (hn : p₂ p₃) (h : p₂ = p₃) :
p₂ = real.pi - 2 p₃

The angle at the apex of an isosceles triangle is `π` minus twice a base angle, oriented angle-at-point form.

theorem euclidean_geometry.abs_oangle_right_to_real_lt_pi_div_two_of_dist_eq {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₂ = p₃) :
| p₃).to_real| <

A base angle of an isosceles triangle is acute, oriented angle-at-point form.

theorem euclidean_geometry.abs_oangle_left_to_real_lt_pi_div_two_of_dist_eq {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₂ = p₃) :
| p₁).to_real| <

A base angle of an isosceles triangle is acute, oriented angle-at-point form.

theorem euclidean_geometry.cos_oangle_eq_cos_angle {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p p₁ p₂ : P} (hp₁ : p₁ p) (hp₂ : p₂ p) :
p₂).cos = real.cos p₂)

The cosine of the oriented angle at `p` between two points not equal to `p` equals that of the unoriented angle.

theorem euclidean_geometry.oangle_eq_angle_or_eq_neg_angle {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p p₁ p₂ : P} (hp₁ : p₁ p) (hp₂ : p₂ p) :
p₂ = p₂) p₂ = - p₂)

The oriented angle at `p` between two points not equal to `p` is plus or minus the unoriented angle.

theorem euclidean_geometry.angle_eq_abs_oangle_to_real {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p p₁ p₂ : P} (hp₁ : p₁ p) (hp₂ : p₂ p) :
p₂ = | p₂).to_real|

The unoriented angle at `p` between two points not equal to `p` is the absolute value of the oriented angle.

theorem euclidean_geometry.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p p₁ p₂ : P} (h : p₂).sign = 0) :
p₁ = p p₂ = p p₂ = 0 p₂ = real.pi

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 π.

theorem euclidean_geometry.oangle_eq_of_angle_eq_of_sign_eq {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P} (h : p₃ = p₆) (hs : p₃).sign = p₆).sign) :
p₃ = p₆

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).

theorem euclidean_geometry.angle_eq_iff_oangle_eq_of_sign_eq {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P} (hp₁ : p₁ p₂) (hp₃ : p₃ p₂) (hp₄ : p₄ p₅) (hp₆ : p₆ p₅) (hs : p₃).sign = p₆).sign) :
p₃ = p₆ p₃ = p₆

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.

theorem euclidean_geometry.oangle_eq_angle_of_sign_eq_one {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃).sign = 1) :
p₃ = p₂ p₃)

The oriented angle between three points equals the unoriented angle if the sign is positive.

theorem euclidean_geometry.oangle_eq_neg_angle_of_sign_eq_neg_one {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃).sign = -1) :
p₃ = - p₂ p₃)

The oriented angle between three points equals minus the unoriented angle if the sign is negative.

theorem euclidean_geometry.oangle_eq_zero_iff_angle_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p p₁ p₂ : P} (hp₁ : p₁ p) (hp₂ : p₂ p) :
p₂ = 0 p₂ = 0

The unoriented angle at `p` between two points not equal to `p` is zero if and only if the unoriented angle is zero.

theorem euclidean_geometry.oangle_eq_pi_iff_angle_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} :
p₃ = real.pi p₃ = real.pi

The oriented angle between three points is `π` if and only if the unoriented angle is `π`.

theorem euclidean_geometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₃ =

If the oriented angle between three points is `π / 2`, so is the unoriented angle.

theorem euclidean_geometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₁ =

If the oriented angle between three points is `π / 2`, so is the unoriented angle (reversed).

theorem euclidean_geometry.angle_eq_pi_div_two_of_oangle_eq_neg_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (-real.pi / 2)) :
p₃ =

If the oriented angle between three points is `-π / 2`, the unoriented angle is `π / 2`.

theorem euclidean_geometry.angle_rev_eq_pi_div_two_of_oangle_eq_neg_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (-real.pi / 2)) :
p₁ =

If the oriented angle between three points is `-π / 2`, the unoriented angle (reversed) is `π / 2`.

theorem euclidean_geometry.oangle_swap₁₂_sign {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] (p₁ p₂ p₃ : P) :
- p₃).sign = p₃).sign

Swapping the first and second points in an oriented angle negates the sign of that angle.

theorem euclidean_geometry.oangle_swap₁₃_sign {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] (p₁ p₂ p₃ : P) :
- p₃).sign = p₁).sign

Swapping the first and third points in an oriented angle negates the sign of that angle.

theorem euclidean_geometry.oangle_swap₂₃_sign {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] (p₁ p₂ p₃ : P) :
- p₃).sign = p₂).sign

Swapping the second and third points in an oriented angle negates the sign of that angle.

theorem euclidean_geometry.oangle_rotate_sign {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] (p₁ p₂ p₃ : P) :
p₁).sign = p₃).sign

Rotating the points in an oriented angle does not change the sign of that angle.

theorem euclidean_geometry.oangle_eq_pi_iff_sbtw {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} :
p₃ = real.pi p₁ p₂ p₃

The oriented angle between three points is π if and only if the second point is strictly between the other two.

theorem sbtw.oangle₁₂₃_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) :

If the second of three points is strictly between the other two, the oriented angle at that point is π.

theorem sbtw.oangle₃₂₁_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) :

If the second of three points is strictly between the other two, the oriented angle at that point (reversed) is π.

theorem wbtw.oangle₂₁₃_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) :
p₃ = 0

If the second of three points is weakly between the other two, the oriented angle at the first point is zero.

theorem sbtw.oangle₂₁₃_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) :
p₃ = 0

If the second of three points is strictly between the other two, the oriented angle at the first point is zero.

theorem wbtw.oangle₃₁₂_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) :
p₂ = 0

If the second of three points is weakly between the other two, the oriented angle at the first point (reversed) is zero.

theorem sbtw.oangle₃₁₂_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) :
p₂ = 0

If the second of three points is strictly between the other two, the oriented angle at the first point (reversed) is zero.

theorem wbtw.oangle₂₃₁_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) :
p₁ = 0

If the second of three points is weakly between the other two, the oriented angle at the third point is zero.

theorem sbtw.oangle₂₃₁_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) :
p₁ = 0

If the second of three points is strictly between the other two, the oriented angle at the third point is zero.

theorem wbtw.oangle₁₃₂_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) :
p₂ = 0

If the second of three points is weakly between the other two, the oriented angle at the third point (reversed) is zero.

theorem sbtw.oangle₁₃₂_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) :
p₂ = 0

If the second of three points is strictly between the other two, the oriented angle at the third point (reversed) is zero.

theorem euclidean_geometry.oangle_eq_zero_iff_wbtw {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} :
p₃ = 0 p₂ p₁ p₃ p₂ p₃ p₁

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.

theorem wbtw.oangle_eq_left {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₁' p₂ p₃ : P} (h : p₂ p₁ p₁') (hp₁p₂ : p₁ p₂) :
p₃ = p₃

An oriented angle is unchanged by replacing the first point by one weakly further away on the same ray.

theorem sbtw.oangle_eq_left {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₁' p₂ p₃ : P} (h : p₂ p₁ p₁') :
p₃ = p₃

An oriented angle is unchanged by replacing the first point by one strictly further away on the same ray.

theorem wbtw.oangle_eq_right {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ p₃' : P} (h : p₂ p₃ p₃') (hp₃p₂ : p₃ p₂) :
p₃ = p₃'

An oriented angle is unchanged by replacing the third point by one weakly further away on the same ray.

theorem sbtw.oangle_eq_right {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ p₃' : P} (h : p₂ p₃ p₃') :
p₃ = p₃'

An oriented angle is unchanged by replacing the third point by one strictly further away on the same ray.

@[simp]
theorem euclidean_geometry.oangle_midpoint_left {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] (p₁ p₂ p₃ : P) :
euclidean_geometry.oangle p₁ p₂) p₂ p₃ = p₃

An oriented angle is unchanged by replacing the first point with the midpoint of the segment between it and the second point.

@[simp]
theorem euclidean_geometry.oangle_midpoint_rev_left {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] (p₁ p₂ p₃ : P) :
euclidean_geometry.oangle p₂ p₁) p₂ p₃ = p₃

An oriented angle is unchanged by replacing the first point with the midpoint of the segment between the second point and that point.

@[simp]
theorem euclidean_geometry.oangle_midpoint_right {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] (p₁ p₂ p₃ : P) :
p₃ p₂) = p₃

An oriented angle is unchanged by replacing the third point with the midpoint of the segment between it and the second point.

@[simp]
theorem euclidean_geometry.oangle_midpoint_rev_right {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] (p₁ p₂ p₃ : P) :
p₂ p₃) = p₃

An oriented angle is unchanged by replacing the third point with the midpoint of the segment between the second point and that point.

theorem sbtw.oangle_eq_add_pi_left {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₁' p₂ p₃ : P} (h : p₁ p₂ p₁') (hp₃p₂ : p₃ p₂) :
p₃ = p₃ + real.pi

Replacing the first point by one on the same line but the opposite ray adds π to the oriented angle.

theorem sbtw.oangle_eq_add_pi_right {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ p₃' : P} (h : p₃ p₂ p₃') (hp₁p₂ : p₁ p₂) :
p₃ = p₃' + real.pi

Replacing the third point by one on the same line but the opposite ray adds π to the oriented angle.

theorem sbtw.oangle_eq_left_right {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₁' p₂ p₃ p₃' : P} (h₁ : p₁ p₂ p₁') (h₃ : p₃ p₂ p₃') :
p₃ = p₃'

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).

theorem collinear.two_zsmul_oangle_eq_left {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₁' p₂ p₃ : P} (h : {p₁, p₂, p₁'}) (hp₁p₂ : p₁ p₂) (hp₁'p₂ : p₁' p₂) :
2 p₃ = 2 p₃

Replacing the first point by one on the same line does not change twice the oriented angle.

theorem collinear.two_zsmul_oangle_eq_right {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ p₃' : P} (h : {p₃, p₂, p₃'}) (hp₃p₂ : p₃ p₂) (hp₃'p₂ : p₃' p₂) :
2 p₃ = 2 p₃'

Replacing the third point by one on the same line does not change twice the oriented angle.

theorem euclidean_geometry.dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p : P} (h : p₁ p₂) :
p = p (r : ), r (p₂ -ᵥ p₁) +ᵥ p₁ p₂ = p

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.

theorem collinear.oangle_sign_of_same_ray_vsub {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ p₄ : P} (p₅ : P) (hp₁p₂ : p₁ p₂) (hp₃p₄ : p₃ p₄) (hc : {p₁, p₂, p₃, p₄}) (hr : (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)) :
p₂).sign = p₄).sign

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.

theorem sbtw.oangle_sign_eq {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (p₄ : P) (h : p₁ p₂ p₃) :
p₂).sign = p₃).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.

theorem wbtw.oangle_sign_eq_of_ne_left {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (p₄ : P) (h : p₁ p₂ p₃) (hne : p₁ p₂) :
p₂).sign = p₃).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.

theorem sbtw.oangle_sign_eq_left {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (p₄ : P) (h : p₁ p₂ p₃) :
p₂).sign = p₃).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.

theorem wbtw.oangle_sign_eq_of_ne_right {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (p₄ : P) (h : p₁ p₂ p₃) (hne : p₂ p₃) :
p₃).sign = p₃).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.

theorem sbtw.oangle_sign_eq_right {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {p₁ p₂ p₃ : P} (p₄ : P) (h : p₁ p₂ p₃) :
p₃).sign = p₃).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.

theorem affine_subspace.s_same_side.oangle_sign_eq {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {s : P} {p₁ p₂ p₃ p₄ : P} (hp₁ : p₁ s) (hp₂ : p₂ s) (hp₃p₄ : s.s_same_side p₃ p₄) :
p₂).sign = p₂).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.

theorem affine_subspace.s_opp_side.oangle_sign_eq_neg {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact ] [ (fin 2)] {s : P} {p₁ p₂ p₃ p₄ : P} (hp₁ : p₁ s) (hp₂ : p₂ s) (hp₃p₄ : s.s_opp_side p₃ p₄) :
p₂).sign = - p₂).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.