mathlib3 documentation

geometry.euclidean.angle.oriented.affine

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 #

noncomputable def euclidean_geometry.oangle {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (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
theorem euclidean_geometry.continuous_at_oangle {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {x : P × P × P} (hx12 : x.fst x.snd.fst) (hx32 : x.snd.snd x.snd.fst) :

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] (p₁ p₂ : P) :
euclidean_geometry.oangle 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] (p₁ p₂ : P) :
euclidean_geometry.oangle 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] (p₁ p₂ : P) :
euclidean_geometry.oangle 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : (euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : (euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : (euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : (euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : (euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : (euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : (euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : (euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : (euclidean_geometry.oangle p₁ p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] (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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] (p₁ p₂ p₃ : P) :
euclidean_geometry.oangle p₁ p₂ p₃ + euclidean_geometry.oangle p₃ p₂ p₁ = 0

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.

theorem euclidean_geometry.oangle_eq_zero_or_eq_pi_iff_collinear {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} :
euclidean_geometry.oangle p₁ p₂ p₃ = 0 euclidean_geometry.oangle p₁ p₂ p₃ = real.pi collinear {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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P} (h : 2 euclidean_geometry.oangle p₁ p₂ p₃ = 2 euclidean_geometry.oangle p₄ p₅ p₆) :
affine_independent ![p₁, p₂, p₃] affine_independent ![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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P} (h : 2 euclidean_geometry.oangle p₁ p₂ p₃ = 2 euclidean_geometry.oangle p₄ p₅ p₆) :
collinear {p₁, p₂, p₃} collinear {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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P} (h₁₂₄₅ : vector_span {p₁, p₂} = vector_span {p₄, p₅}) (h₃₂₆₅ : vector_span {p₃, p₂} = vector_span {p₆, p₅}) :
2 euclidean_geometry.oangle p₁ p₂ p₃ = 2 euclidean_geometry.oangle p₄ p₅ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P} (h₁₂₄₅ : (affine_span {p₁, p₂}).parallel (affine_span {p₄, p₅})) (h₃₂₆₅ : (affine_span {p₃, p₂}).parallel (affine_span {p₆, p₅})) :
2 euclidean_geometry.oangle p₁ p₂ p₃ = 2 euclidean_geometry.oangle p₄ p₅ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p p₁ p₂ p₃ : P} (hp₁ : p₁ p) (hp₂ : p₂ p) (hp₃ : 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p p₁ p₂ p₃ : P} (hp₁ : p₁ p) (hp₂ : p₂ p) (hp₃ : 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p p₁ p₂ p₃ : P} (hp₁ : p₁ p) (hp₂ : p₂ p) (hp₃ : 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p p₁ p₂ p₃ : P} (hp₁ : p₁ p) (hp₂ : p₂ p) (hp₃ : 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p p₁ p₂ p₃ : P} (hp₁ : p₁ p) (hp₂ : p₂ p) (hp₃ : p₃ p) :

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : has_dist.dist p₁ p₂ = has_dist.dist 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (hn : p₂ p₃) (h : has_dist.dist p₁ p₂ = has_dist.dist p₁ p₃) :

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.

theorem euclidean_geometry.cos_oangle_eq_cos_angle {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p p₁ p₂ : P} (hp₁ : p₁ p) (hp₂ : p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p p₁ p₂ : P} (hp₁ : p₁ p) (hp₂ : 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p p₁ p₂ : P} (hp₁ : p₁ p) (hp₂ : p₂ p) :

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

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

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P} (hp₁ : p₁ p₂) (hp₃ : p₃ p₂) (hp₄ : p₄ p₅) (hp₆ : p₆ p₅) (hs : (euclidean_geometry.oangle p₁ p₂ p₃).sign = (euclidean_geometry.oangle p₄ p₅ p₆).sign) :

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : (euclidean_geometry.oangle p₁ p₂ p₃).sign = 1) :

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : (euclidean_geometry.oangle p₁ p₂ p₃).sign = -1) :

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p p₁ p₂ : P} (hp₁ : p₁ p) (hp₂ : p₂ p) :

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.

theorem euclidean_geometry.oangle_swap₁₂_sign {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] (p₁ p₂ p₃ : P) :

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] (p₁ p₂ p₃ : P) :

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] (p₁ p₂ p₃ : P) :

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] (p₁ p₂ p₃ : P) :

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} :
euclidean_geometry.oangle p₁ p₂ p₃ = real.pi sbtw 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : sbtw 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : sbtw 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : wbtw p₁ p₂ p₃) :
euclidean_geometry.oangle 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : sbtw p₁ p₂ p₃) :
euclidean_geometry.oangle 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : wbtw p₁ p₂ p₃) :
euclidean_geometry.oangle 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : sbtw p₁ p₂ p₃) :
euclidean_geometry.oangle 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : wbtw p₁ p₂ p₃) :
euclidean_geometry.oangle 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : sbtw p₁ p₂ p₃) :
euclidean_geometry.oangle 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : wbtw p₁ p₂ p₃) :
euclidean_geometry.oangle 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (h : sbtw p₁ p₂ p₃) :
euclidean_geometry.oangle 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} :
euclidean_geometry.oangle p₁ p₂ p₃ = 0 wbtw p₂ p₁ p₃ wbtw 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₁' p₂ p₃ : P} (h : wbtw p₂ p₁ p₁') (hp₁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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₁' p₂ p₃ : P} (h : sbtw 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ p₃' : P} (h : wbtw p₂ p₃ p₃') (hp₃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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ p₃' : P} (h : sbtw 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] (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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] (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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] (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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] (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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₁' p₂ p₃ : P} (h : sbtw p₁ p₂ p₁') (hp₃p₂ : p₃ p₂) :

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ p₃' : P} (h : sbtw p₃ p₂ p₃') (hp₁p₂ : p₁ p₂) :

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₁' p₂ p₃ p₃' : P} (h₁ : sbtw p₁ p₂ p₁') (h₃ : sbtw p₃ p₂ p₃') :
euclidean_geometry.oangle p₁ p₂ p₃ = euclidean_geometry.oangle 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₁' p₂ p₃ : P} (h : collinear {p₁, p₂, p₁'}) (hp₁p₂ : p₁ p₂) (hp₁'p₂ : p₁' p₂) :
2 euclidean_geometry.oangle p₁ p₂ p₃ = 2 euclidean_geometry.oangle p₁' p₂ 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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ p₃' : P} (h : collinear {p₃, p₂, p₃'}) (hp₃p₂ : p₃ p₂) (hp₃'p₂ : p₃' p₂) :
2 euclidean_geometry.oangle p₁ p₂ p₃ = 2 euclidean_geometry.oangle p₁ p₂ p₃'

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.

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

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (p₄ : P) (h : sbtw p₁ p₂ p₃) :

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (p₄ : P) (h : wbtw p₁ p₂ p₃) (hne : p₁ p₂) :

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (p₄ : P) (h : sbtw p₁ p₂ p₃) :

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (p₄ : P) (h : wbtw p₁ p₂ p₃) (hne : p₂ p₃) :

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {p₁ p₂ p₃ : P} (p₄ : P) (h : sbtw p₁ p₂ p₃) :

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {s : affine_subspace P} {p₁ p₂ p₃ p₄ : P} (hp₁ : p₁ s) (hp₂ : p₂ s) (hp₃p₄ : s.s_same_side p₃ p₄) :

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented V (fin 2)] {s : affine_subspace P} {p₁ p₂ p₃ p₄ : P} (hp₁ : p₁ s) (hp₂ : p₂ s) (hp₃p₄ : s.s_opp_side p₃ p₄) :

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.