mathlib documentation

geometry.euclidean.oriented_angle

Oriented angles. #

This file defines oriented angles in real inner product spaces.

Main definitions #

Implementation notes #

The definitions here use the real.angle type, angles modulo 2 * π. For some purposes, angles modulo π are more convenient, because results are true for such angles with less configuration dependence. Results that are only equalities modulo π can be represented modulo 2 * π as equalities of (2 : ℤ) • θ.

Definitions and results in the orthonormal namespace, with respect to a particular choice of orthonormal basis, are mainly for use in setting up the API and proving that certain definitions do not depend on the choice of basis for a given orientation. Applications should generally use the definitions and results in the orientation namespace instead.

References #

noncomputable def orthonormal.oangle {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) :

The oriented angle from x to y, modulo 2 * π. If either vector is 0, this is 0.

Equations
theorem orthonormal.continuous_at_oangle {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x : V × V} (hx1 : x.fst 0) (hx2 : x.snd 0) :
continuous_at (λ (y : V × V), hb.oangle y.fst y.snd) x

Oriented angles are continuous when the vectors involved are nonzero.

@[simp]
theorem orthonormal.oangle_zero_left {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x : V) :
hb.oangle 0 x = 0

If the first vector passed to oangle is 0, the result is 0.

@[simp]
theorem orthonormal.oangle_zero_right {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x : V) :
hb.oangle x 0 = 0

If the second vector passed to oangle is 0, the result is 0.

@[simp]
theorem orthonormal.oangle_self {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x : V) :
hb.oangle x x = 0

If the two vectors passed to oangle are the same, the result is 0.

theorem orthonormal.oangle_rev {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) :
hb.oangle y x = -hb.oangle x y

Swapping the two vectors passed to oangle negates the angle.

@[simp]
theorem orthonormal.oangle_add_oangle_rev {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) :
hb.oangle x y + hb.oangle y x = 0

Adding the angles between two vectors in each order results in 0.

theorem orthonormal.oangle_neg_left {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} (hx : x 0) (hy : y 0) :
hb.oangle (-x) y = hb.oangle x y + real.pi

Negating the first vector passed to oangle adds π to the angle.

theorem orthonormal.oangle_neg_right {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} (hx : x 0) (hy : y 0) :
hb.oangle x (-y) = hb.oangle x y + real.pi

Negating the second vector passed to oangle adds π to the angle.

@[simp]
theorem orthonormal.two_zsmul_oangle_neg_left {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) :
2 hb.oangle (-x) y = 2 hb.oangle x y

Negating the first vector passed to oangle does not change twice the angle.

@[simp]
theorem orthonormal.two_zsmul_oangle_neg_right {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) :
2 hb.oangle x (-y) = 2 hb.oangle x y

Negating the second vector passed to oangle does not change twice the angle.

@[simp]
theorem orthonormal.oangle_neg_neg {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) :
hb.oangle (-x) (-y) = hb.oangle x y

Negating both vectors passed to oangle does not change the angle.

theorem orthonormal.oangle_neg_left_eq_neg_right {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) :
hb.oangle (-x) y = hb.oangle x (-y)

Negating the first vector produces the same angle as negating the second vector.

@[simp]
theorem orthonormal.oangle_neg_self_left {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x : V} (hx : x 0) :

The angle between the negation of a nonzero vector and that vector is π.

@[simp]
theorem orthonormal.oangle_neg_self_right {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x : V} (hx : x 0) :

The angle between a nonzero vector and its negation is π.

@[simp]
theorem orthonormal.two_zsmul_oangle_neg_self_left {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x : V) :
2 hb.oangle (-x) x = 0

Twice the angle between the negation of a vector and that vector is 0.

@[simp]
theorem orthonormal.two_zsmul_oangle_neg_self_right {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x : V) :
2 hb.oangle x (-x) = 0

Twice the angle between a vector and its negation is 0.

@[simp]
theorem orthonormal.oangle_add_oangle_rev_neg_left {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) :
hb.oangle (-x) y + hb.oangle (-y) x = 0

Adding the angles between two vectors in each order, with the first vector in each angle negated, results in 0.

@[simp]
theorem orthonormal.oangle_add_oangle_rev_neg_right {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) :
hb.oangle x (-y) + hb.oangle y (-x) = 0

Adding the angles between two vectors in each order, with the second vector in each angle negated, results in 0.

@[simp]
theorem orthonormal.oangle_smul_left_of_pos {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) {r : } (hr : 0 < r) :
hb.oangle (r x) y = hb.oangle x y

Multiplying the first vector passed to oangle by a positive real does not change the angle.

@[simp]
theorem orthonormal.oangle_smul_right_of_pos {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) {r : } (hr : 0 < r) :
hb.oangle x (r y) = hb.oangle x y

Multiplying the second vector passed to oangle by a positive real does not change the angle.

@[simp]
theorem orthonormal.oangle_smul_left_of_neg {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) {r : } (hr : r < 0) :
hb.oangle (r x) y = hb.oangle (-x) y

Multiplying the first vector passed to oangle by a negative real produces the same angle as negating that vector.

@[simp]
theorem orthonormal.oangle_smul_right_of_neg {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) {r : } (hr : r < 0) :
hb.oangle x (r y) = hb.oangle x (-y)

Multiplying the second vector passed to oangle by a negative real produces the same angle as negating that vector.

@[simp]
theorem orthonormal.oangle_smul_left_self_of_nonneg {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x : V) {r : } (hr : 0 r) :
hb.oangle (r x) x = 0

The angle between a nonnegative multiple of a vector and that vector is 0.

@[simp]
theorem orthonormal.oangle_smul_right_self_of_nonneg {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x : V) {r : } (hr : 0 r) :
hb.oangle x (r x) = 0

The angle between a vector and a nonnegative multiple of that vector is 0.

@[simp]
theorem orthonormal.oangle_smul_smul_self_of_nonneg {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x : V) {r₁ r₂ : } (hr₁ : 0 r₁) (hr₂ : 0 r₂) :
hb.oangle (r₁ x) (r₂ x) = 0

The angle between two nonnegative multiples of the same vector is 0.

@[simp]
theorem orthonormal.two_zsmul_oangle_smul_left_of_ne_zero {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) {r : } (hr : r 0) :
2 hb.oangle (r x) y = 2 hb.oangle x y

Multiplying the first vector passed to oangle by a nonzero real does not change twice the angle.

@[simp]
theorem orthonormal.two_zsmul_oangle_smul_right_of_ne_zero {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) {r : } (hr : r 0) :
2 hb.oangle x (r y) = 2 hb.oangle x y

Multiplying the second vector passed to oangle by a nonzero real does not change twice the angle.

@[simp]
theorem orthonormal.two_zsmul_oangle_smul_left_self {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x : V) {r : } :
2 hb.oangle (r x) x = 0

Twice the angle between a multiple of a vector and that vector is 0.

@[simp]
theorem orthonormal.two_zsmul_oangle_smul_right_self {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x : V) {r : } :
2 hb.oangle x (r x) = 0

Twice the angle between a vector and a multiple of that vector is 0.

@[simp]
theorem orthonormal.two_zsmul_oangle_smul_smul_self {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x : V) {r₁ r₂ : } :
2 hb.oangle (r₁ x) (r₂ x) = 0

Twice the angle between two multiples of a vector is 0.

theorem orthonormal.oangle_eq_zero_iff_oangle_rev_eq_zero {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} :
hb.oangle x y = 0 hb.oangle y x = 0

The oriented angle between two vectors is zero if and only if the angle with the vectors swapped is zero.

theorem orthonormal.oangle_eq_zero_iff_same_ray {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} :
hb.oangle x y = 0 same_ray x y

The oriented angle between two vectors is zero if and only if they are on the same ray.

theorem orthonormal.oangle_eq_pi_iff_oangle_rev_eq_pi {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} :

The oriented angle between two vectors is π if and only if the angle with the vectors swapped is π.

theorem orthonormal.oangle_eq_pi_iff_same_ray_neg {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} :
hb.oangle x y = real.pi x 0 y 0 same_ray x (-y)

The oriented angle between two vectors is π if and only they are nonzero and the first is on the same ray as the negation of the second.

The oriented angle between two vectors is zero or π if and only if those two vectors are not linearly independent.

theorem orthonormal.oangle_eq_zero_or_eq_pi_iff_right_eq_smul {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} :
hb.oangle x y = 0 hb.oangle x y = real.pi x = 0 ∃ (r : ), y = r x

The oriented angle between two vectors is zero or π if and only if the first vector is zero or the second is a multiple of the first.

The oriented angle between two vectors is not zero or π if and only if those two vectors are linearly independent.

theorem orthonormal.eq_iff_norm_eq_and_oangle_eq_zero {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) :
x = y x = y hb.oangle x y = 0

Two vectors are equal if and only if they have equal norms and zero angle between them.

theorem orthonormal.eq_iff_oangle_eq_zero_of_norm_eq {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} (h : x = y) :
x = y hb.oangle x y = 0

Two vectors with equal norms are equal if and only if they have zero angle between them.

theorem orthonormal.eq_iff_norm_eq_of_oangle_eq_zero {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} (h : hb.oangle x y = 0) :

Two vectors with zero angle between them are equal if and only if they have equal norms.

@[simp]
theorem orthonormal.oangle_add {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y z : V} (hx : x 0) (hy : y 0) (hz : z 0) :
hb.oangle x y + hb.oangle y z = hb.oangle x z

Given three nonzero vectors, the angle between the first and the second plus the angle between the second and the third equals the angle between the first and the third.

@[simp]
theorem orthonormal.oangle_add_swap {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y z : V} (hx : x 0) (hy : y 0) (hz : z 0) :
hb.oangle y z + hb.oangle x y = hb.oangle x z

Given three nonzero vectors, the angle between the second and the third plus the angle between the first and the second equals the angle between the first and the third.

@[simp]
theorem orthonormal.oangle_sub_left {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y z : V} (hx : x 0) (hy : y 0) (hz : z 0) :
hb.oangle x z - hb.oangle x y = hb.oangle y z

Given three nonzero vectors, the angle between the first and the third minus the angle between the first and the second equals the angle between the second and the third.

@[simp]
theorem orthonormal.oangle_sub_right {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y z : V} (hx : x 0) (hy : y 0) (hz : z 0) :
hb.oangle x z - hb.oangle y z = hb.oangle x y

Given three nonzero vectors, the angle between the first and the third minus the angle between the second and the third equals the angle between the first and the second.

@[simp]
theorem orthonormal.oangle_add_cyc3 {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y z : V} (hx : x 0) (hy : y 0) (hz : z 0) :
hb.oangle x y + hb.oangle y z + hb.oangle z x = 0

Given three nonzero vectors, adding the angles between them in cyclic order results in 0.

@[simp]
theorem orthonormal.oangle_add_cyc3_neg_left {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y z : V} (hx : x 0) (hy : y 0) (hz : z 0) :
hb.oangle (-x) y + hb.oangle (-y) z + hb.oangle (-z) x = real.pi

Given three nonzero vectors, adding the angles between them in cyclic order, with the first vector in each angle negated, results in π. If the vectors add to 0, this is a version of the sum of the angles of a triangle.

@[simp]
theorem orthonormal.oangle_add_cyc3_neg_right {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y z : V} (hx : x 0) (hy : y 0) (hz : z 0) :
hb.oangle x (-y) + hb.oangle y (-z) + hb.oangle z (-x) = real.pi

Given three nonzero vectors, adding the angles between them in cyclic order, with the second vector in each angle negated, results in π. If the vectors add to 0, this is a version of the sum of the angles of a triangle.

theorem orthonormal.oangle_sub_eq_oangle_sub_rev_of_norm_eq {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} (h : x = y) :
hb.oangle x (x - y) = hb.oangle (y - x) y

Pons asinorum, oriented vector angle form.

theorem orthonormal.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} (hn : x y) (h : x = y) :
hb.oangle y x = real.pi - 2 hb.oangle (y - x) y

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

theorem orthonormal.oangle_eq_two_zsmul_oangle_sub_of_norm_eq {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y z : V} (hxyne : x y) (hxzne : x z) (hxy : x = y) (hxz : x = z) :
hb.oangle y z = 2 hb.oangle (y - x) (z - x)

Angle at center of a circle equals twice angle at circumference, oriented vector angle form.

theorem orthonormal.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y z : V} (hxyne : x y) (hxzne : x z) {r : } (hx : x = r) (hy : y = r) (hz : z = r) :
hb.oangle y z = 2 hb.oangle (y - x) (z - x)

Angle at center of a circle equals twice angle at circumference, oriented vector angle form with radius specified.

theorem orthonormal.two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x₁ x₂ y z : V} (hx₁yne : x₁ y) (hx₁zne : x₁ z) (hx₂yne : x₂ y) (hx₂zne : x₂ z) {r : } (hx₁ : x₁ = r) (hx₂ : x₂ = r) (hy : y = r) (hz : z = r) :
2 hb.oangle (y - x₁) (z - x₁) = 2 hb.oangle (y - x₂) (z - x₂)

Oriented vector angle version of "angles in same segment are equal" and "opposite angles of a cyclic quadrilateral add to π", for oriented angles mod π (for which those are the same result), represented here as equality of twice the angles.

noncomputable def orthonormal.rotation {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (θ : real.angle) :

A rotation by the oriented angle θ.

Equations
@[simp]

The determinant of rotation (as a linear map) is equal to 1.

@[simp]

The determinant of rotation (as a linear equiv) is equal to 1.

@[simp]
theorem orthonormal.rotation_symm {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (θ : real.angle) :
(hb.rotation θ).symm = hb.rotation (-θ)

The inverse of rotation is rotation by the negation of the angle.

@[simp]

Rotation by 0 is the identity.

Rotation by π is negation.

@[simp]
theorem orthonormal.rotation_trans {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (θ₁ θ₂ : real.angle) :
(hb.rotation θ₁).trans (hb.rotation θ₂) = hb.rotation (θ₂ + θ₁)

Rotating twice is equivalent to rotating by the sum of the angles.

@[simp]
theorem orthonormal.oangle_rotation_left {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} (hx : x 0) (hy : y 0) (θ : real.angle) :
hb.oangle ((hb.rotation θ) x) y = hb.oangle x y - θ

Rotating the first vector by θ subtracts θ from the angle between two vectors.

@[simp]
theorem orthonormal.oangle_rotation_right {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} (hx : x 0) (hy : y 0) (θ : real.angle) :
hb.oangle x ((hb.rotation θ) y) = hb.oangle x y + θ

Rotating the second vector by θ adds θ to the angle between two vectors.

@[simp]
theorem orthonormal.oangle_rotation_self_left {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x : V} (hx : x 0) (θ : real.angle) :
hb.oangle ((hb.rotation θ) x) x = -θ

The rotation of a vector by θ has an angle of from that vector.

@[simp]
theorem orthonormal.oangle_rotation_self_right {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x : V} (hx : x 0) (θ : real.angle) :
hb.oangle x ((hb.rotation θ) x) = θ

A vector has an angle of θ from the rotation of that vector by θ.

@[simp]
theorem orthonormal.oangle_rotation_oangle_left {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) :
hb.oangle ((hb.rotation (hb.oangle x y)) x) y = 0

Rotating the first vector by the angle between the two vectors results an an angle of 0.

@[simp]
theorem orthonormal.oangle_rotation_oangle_right {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) :
hb.oangle y ((hb.rotation (hb.oangle x y)) x) = 0

Rotating the first vector by the angle between the two vectors and swapping the vectors results an an angle of 0.

@[simp]
theorem orthonormal.oangle_rotation {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) (θ : real.angle) :
hb.oangle ((hb.rotation θ) x) ((hb.rotation θ) y) = hb.oangle x y

Rotating both vectors by the same angle does not change the angle between those vectors.

@[simp]
theorem orthonormal.rotation_eq_self_iff_angle_eq_zero {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x : V} (hx : x 0) (θ : real.angle) :
(hb.rotation θ) x = x θ = 0

A rotation of a nonzero vector equals that vector if and only if the angle is zero.

@[simp]
theorem orthonormal.eq_rotation_self_iff_angle_eq_zero {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x : V} (hx : x 0) (θ : real.angle) :
x = (hb.rotation θ) x θ = 0

A nonzero vector equals a rotation of that vector if and only if the angle is zero.

theorem orthonormal.rotation_eq_self_iff {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x : V) (θ : real.angle) :
(hb.rotation θ) x = x x = 0 θ = 0

A rotation of a vector equals that vector if and only if the vector or the angle is zero.

theorem orthonormal.eq_rotation_self_iff {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x : V) (θ : real.angle) :
x = (hb.rotation θ) x x = 0 θ = 0

A vector equals a rotation of that vector if and only if the vector or the angle is zero.

@[simp]
theorem orthonormal.rotation_oangle_eq_iff_norm_eq {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) :
(hb.rotation (hb.oangle x y)) x = y x = y

Rotating a vector by the angle to another vector gives the second vector if and only if the norms are equal.

theorem orthonormal.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} (hx : x 0) (hy : y 0) (θ : real.angle) :
hb.oangle x y = θ y = (y / x) (hb.rotation θ) x

The angle between two nonzero vectors is θ if and only if the second vector is the first rotated by θ and scaled by the ratio of the norms.

theorem orthonormal.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} (hx : x 0) (hy : y 0) (θ : real.angle) :
hb.oangle x y = θ ∃ (r : ), 0 < r y = r (hb.rotation θ) x

The angle between two nonzero vectors is θ if and only if the second vector is the first rotated by θ and scaled by a positive real.

theorem orthonormal.oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} (θ : real.angle) :
hb.oangle x y = θ x 0 y 0 y = (y / x) (hb.rotation θ) x θ = 0 (x = 0 y = 0)

The angle between two vectors is θ if and only if they are nonzero and the second vector is the first rotated by θ and scaled by the ratio of the norms, or θ and at least one of the vectors are zero.

theorem orthonormal.oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} (θ : real.angle) :
hb.oangle x y = θ (x 0 y 0 ∃ (r : ), 0 < r y = r (hb.rotation θ) x) θ = 0 (x = 0 y = 0)

The angle between two vectors is θ if and only if they are nonzero and the second vector is the first rotated by θ and scaled by a positive real, or θ and at least one of the vectors are zero.

noncomputable def orthonormal.conj_lie {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) :

Complex conjugation as a linear isometric equivalence in V. Note that this definition depends on the choice of basis, not just on its orientation; for most geometrical purposes, the reflection definitions should be preferred instead.

Equations
@[simp]

The determinant of conj_lie (as a linear map) is equal to -1.

@[simp]

The determinant of conj_lie (as a linear equiv) is equal to -1.

@[simp]
theorem orthonormal.conj_lie_symm {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) :

conj_lie is its own inverse.

@[simp]
theorem orthonormal.oangle_conj_lie {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) :
hb.oangle ((hb.conj_lie) x) ((hb.conj_lie) y) = -hb.oangle x y

Applying conj_lie to both vectors negates the angle between those vectors.

theorem orthonormal.exists_linear_isometry_equiv_eq {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (f : V ≃ₗᵢ[] V) :
∃ (θ : real.angle), f = hb.rotation θ f = hb.conj_lie.trans (hb.rotation θ)

Any linear isometric equivalence in V is rotation or conj_lie composed with rotation.

Any linear isometric equivalence in V with positive determinant is rotation.

Any linear isometric equivalence in V with negative determinant is conj_lie composed with rotation.

theorem orthonormal.exists_linear_isometry_equiv_map_eq_of_orientation_eq {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {b₂ : basis (fin 2) V} (hb₂ : orthonormal b₂) (ho : b.orientation = b₂.orientation) :
∃ (θ : real.angle), b₂ = b.map (hb.rotation θ).to_linear_equiv

Two bases with the same orientation are related by a rotation.

theorem orthonormal.exists_linear_isometry_equiv_map_eq_of_orientation_eq_neg {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {b₂ : basis (fin 2) V} (hb₂ : orthonormal b₂) (ho : b.orientation = -b₂.orientation) :
∃ (θ : real.angle), b₂ = b.map (hb.conj_lie.trans (hb.rotation θ)).to_linear_equiv

Two bases with opposite orientations are related by conj_lie composed with a rotation.

@[simp]
theorem orthonormal.oangle_map {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) (f : V ≃ₗᵢ[] V) :
_.oangle x y = hb.oangle ((f.symm) x) ((f.symm) y)

The angle between two vectors, with respect to a basis given by basis.map with a linear isometric equivalence, equals the angle between those two vectors, transformed by the inverse of that equivalence, with respect to the original basis.

theorem orthonormal.oangle_eq_of_orientation_eq {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {b₂ : basis (fin 2) V} (hb₂ : orthonormal b₂) (ho : b.orientation = b₂.orientation) (x y : V) :
hb.oangle x y = hb₂.oangle x y

The value of oangle does not depend on the choice of basis for a given orientation.

theorem orthonormal.oangle_eq_neg_of_orientation_eq_neg {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {b₂ : basis (fin 2) V} (hb₂ : orthonormal b₂) (ho : b.orientation = -b₂.orientation) (x y : V) :
hb.oangle x y = -hb₂.oangle x y

Negating the orientation negates the value of oangle.

theorem orthonormal.rotation_eq_of_orientation_eq {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {b₂ : basis (fin 2) V} (hb₂ : orthonormal b₂) (ho : b.orientation = b₂.orientation) (θ : real.angle) :
hb.rotation θ = hb₂.rotation θ

rotation does not depend on the choice of basis for a given orientation.

theorem orthonormal.rotation_eq_rotation_neg_of_orientation_eq_neg {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {b₂ : basis (fin 2) V} (hb₂ : orthonormal b₂) (ho : b.orientation = -b₂.orientation) (θ : real.angle) :
hb.rotation θ = hb₂.rotation (-θ)

Negating the orientation negates the angle in rotation.

theorem orthonormal.inner_eq_norm_mul_norm_mul_cos_oangle {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) (x y : V) :

The inner product of two vectors is the product of the norms and the cosine of the oriented angle between the vectors.

theorem orthonormal.cos_oangle_eq_inner_div_norm_mul_norm {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} (hx : x 0) (hy : y 0) :

The cosine of the oriented angle between two nonzero vectors is the inner product divided by the product of the norms.

theorem orthonormal.cos_oangle_eq_cos_angle {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} (hx : x 0) (hy : y 0) :

The cosine of the oriented angle between two nonzero vectors equals that of the unoriented angle.

theorem orthonormal.oangle_eq_angle_or_eq_neg_angle {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} (hx : x 0) (hy : y 0) :

The oriented angle between two nonzero vectors is plus or minus the unoriented angle.

theorem orthonormal.angle_eq_abs_oangle_to_real {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} (hx : x 0) (hy : y 0) :

The unoriented angle between two nonzero vectors is the absolute value of the oriented angle, converted to a real.

If the sign of the oriented angle between two vectors is zero, either one of the vectors is zero or the unoriented angle is 0 or π.

theorem orthonormal.oangle_eq_of_angle_eq_of_sign_eq {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {w x y z : V} (h : inner_product_geometry.angle w x = inner_product_geometry.angle y z) (hs : (hb.oangle w x).sign = (hb.oangle y z).sign) :
hb.oangle w x = hb.oangle y z

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 orthonormal.oangle_eq_iff_angle_eq_of_sign_eq {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {w x y z : V} (hw : w 0) (hx : x 0) (hy : y 0) (hz : z 0) (hs : (hb.oangle w x).sign = (hb.oangle y z).sign) :

If the signs of two oriented angles between nonzero vectors are equal, the oriented angles are equal if and only if the unoriented angles are equal.

theorem orthonormal.oangle_eq_zero_iff_angle_eq_zero {V : Type u_1} [inner_product_space V] {b : basis (fin 2) V} (hb : orthonormal b) {x y : V} (hx : x 0) (hy : y 0) :

The oriented angle between two nonzero vectors is zero if and only if the unoriented angle is zero.

The oriented angle between two vectors is π if and only if the unoriented angle is π.

noncomputable def orientation.oangle {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) :

The oriented angle from x to y, modulo 2 * π. If either vector is 0, this is 0. See inner_product_geometry.angle for the corresponding unoriented angle definition.

Equations
theorem orientation.continuous_at_oangle {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x : V × V} (hx1 : x.fst 0) (hx2 : x.snd 0) :
continuous_at (λ (y : V × V), o.oangle y.fst y.snd) x

Oriented angles are continuous when the vectors involved are nonzero.

@[simp]
theorem orientation.oangle_zero_left {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x : V) :
o.oangle 0 x = 0

If the first vector passed to oangle is 0, the result is 0.

@[simp]
theorem orientation.oangle_zero_right {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x : V) :
o.oangle x 0 = 0

If the second vector passed to oangle is 0, the result is 0.

@[simp]
theorem orientation.oangle_self {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x : V) :
o.oangle x x = 0

If the two vectors passed to oangle are the same, the result is 0.

theorem orientation.oangle_rev {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) :
o.oangle y x = -o.oangle x y

Swapping the two vectors passed to oangle negates the angle.

@[simp]
theorem orientation.oangle_add_oangle_rev {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) :
o.oangle x y + o.oangle y x = 0

Adding the angles between two vectors in each order results in 0.

theorem orientation.oangle_neg_left {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} (hx : x 0) (hy : y 0) :
o.oangle (-x) y = o.oangle x y + real.pi

Negating the first vector passed to oangle adds π to the angle.

theorem orientation.oangle_neg_right {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} (hx : x 0) (hy : y 0) :
o.oangle x (-y) = o.oangle x y + real.pi

Negating the second vector passed to oangle adds π to the angle.

@[simp]
theorem orientation.two_zsmul_oangle_neg_left {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) :
2 o.oangle (-x) y = 2 o.oangle x y

Negating the first vector passed to oangle does not change twice the angle.

@[simp]
theorem orientation.two_zsmul_oangle_neg_right {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) :
2 o.oangle x (-y) = 2 o.oangle x y

Negating the second vector passed to oangle does not change twice the angle.

@[simp]
theorem orientation.oangle_neg_neg {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) :
o.oangle (-x) (-y) = o.oangle x y

Negating both vectors passed to oangle does not change the angle.

theorem orientation.oangle_neg_left_eq_neg_right {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) :
o.oangle (-x) y = o.oangle x (-y)

Negating the first vector produces the same angle as negating the second vector.

@[simp]
theorem orientation.oangle_neg_self_left {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x : V} (hx : x 0) :

The angle between the negation of a nonzero vector and that vector is π.

@[simp]
theorem orientation.oangle_neg_self_right {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x : V} (hx : x 0) :

The angle between a nonzero vector and its negation is π.

@[simp]
theorem orientation.two_zsmul_oangle_neg_self_left {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x : V) :
2 o.oangle (-x) x = 0

Twice the angle between the negation of a vector and that vector is 0.

@[simp]
theorem orientation.two_zsmul_oangle_neg_self_right {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x : V) :
2 o.oangle x (-x) = 0

Twice the angle between a vector and its negation is 0.

@[simp]
theorem orientation.oangle_add_oangle_rev_neg_left {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) :
o.oangle (-x) y + o.oangle (-y) x = 0

Adding the angles between two vectors in each order, with the first vector in each angle negated, results in 0.

@[simp]
theorem orientation.oangle_add_oangle_rev_neg_right {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) :
o.oangle x (-y) + o.oangle y (-x) = 0

Adding the angles between two vectors in each order, with the second vector in each angle negated, results in 0.

@[simp]
theorem orientation.oangle_smul_left_of_pos {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) {r : } (hr : 0 < r) :
o.oangle (r x) y = o.oangle x y

Multiplying the first vector passed to oangle by a positive real does not change the angle.

@[simp]
theorem orientation.oangle_smul_right_of_pos {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) {r : } (hr : 0 < r) :
o.oangle x (r y) = o.oangle x y

Multiplying the second vector passed to oangle by a positive real does not change the angle.

@[simp]
theorem orientation.oangle_smul_left_of_neg {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) {r : } (hr : r < 0) :
o.oangle (r x) y = o.oangle (-x) y

Multiplying the first vector passed to oangle by a negative real produces the same angle as negating that vector.

@[simp]
theorem orientation.oangle_smul_right_of_neg {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) {r : } (hr : r < 0) :
o.oangle x (r y) = o.oangle x (-y)

Multiplying the second vector passed to oangle by a negative real produces the same angle as negating that vector.

@[simp]
theorem orientation.oangle_smul_left_self_of_nonneg {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x : V) {r : } (hr : 0 r) :
o.oangle (r x) x = 0

The angle between a nonnegative multiple of a vector and that vector is 0.

@[simp]
theorem orientation.oangle_smul_right_self_of_nonneg {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x : V) {r : } (hr : 0 r) :
o.oangle x (r x) = 0

The angle between a vector and a nonnegative multiple of that vector is 0.

@[simp]
theorem orientation.oangle_smul_smul_self_of_nonneg {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x : V) {r₁ r₂ : } (hr₁ : 0 r₁) (hr₂ : 0 r₂) :
o.oangle (r₁ x) (r₂ x) = 0

The angle between two nonnegative multiples of the same vector is 0.

@[simp]
theorem orientation.two_zsmul_oangle_smul_left_of_ne_zero {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) {r : } (hr : r 0) :
2 o.oangle (r x) y = 2 o.oangle x y

Multiplying the first vector passed to oangle by a nonzero real does not change twice the angle.

@[simp]
theorem orientation.two_zsmul_oangle_smul_right_of_ne_zero {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) {r : } (hr : r 0) :
2 o.oangle x (r y) = 2 o.oangle x y

Multiplying the second vector passed to oangle by a nonzero real does not change twice the angle.

@[simp]
theorem orientation.two_zsmul_oangle_smul_left_self {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x : V) {r : } :
2 o.oangle (r x) x = 0

Twice the angle between a multiple of a vector and that vector is 0.

@[simp]
theorem orientation.two_zsmul_oangle_smul_right_self {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x : V) {r : } :
2 o.oangle x (r x) = 0

Twice the angle between a vector and a multiple of that vector is 0.

@[simp]
theorem orientation.two_zsmul_oangle_smul_smul_self {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x : V) {r₁ r₂ : } :
2 o.oangle (r₁ x) (r₂ x) = 0

Twice the angle between two multiples of a vector is 0.

theorem orientation.oangle_eq_zero_iff_oangle_rev_eq_zero {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} :
o.oangle x y = 0 o.oangle y x = 0

The oriented angle between two vectors is zero if and only if the angle with the vectors swapped is zero.

theorem orientation.oangle_eq_zero_iff_same_ray {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} :
o.oangle x y = 0 same_ray x y

The oriented angle between two vectors is zero if and only if they are on the same ray.

The oriented angle between two vectors is π if and only if the angle with the vectors swapped is π.

theorem orientation.oangle_eq_pi_iff_same_ray_neg {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} :

The oriented angle between two vectors is π if and only they are nonzero and the first is on the same ray as the negation of the second.

The oriented angle between two vectors is zero or π if and only if those two vectors are not linearly independent.

theorem orientation.oangle_eq_zero_or_eq_pi_iff_right_eq_smul {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} :
o.oangle x y = 0 o.oangle x y = real.pi x = 0 ∃ (r : ), y = r x

The oriented angle between two vectors is zero or π if and only if the first vector is zero or the second is a multiple of the first.

The oriented angle between two vectors is not zero or π if and only if those two vectors are linearly independent.

theorem orientation.eq_iff_norm_eq_and_oangle_eq_zero {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) :
x = y x = y o.oangle x y = 0

Two vectors are equal if and only if they have equal norms and zero angle between them.

theorem orientation.eq_iff_oangle_eq_zero_of_norm_eq {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} (h : x = y) :
x = y o.oangle x y = 0

Two vectors with equal norms are equal if and only if they have zero angle between them.

theorem orientation.eq_iff_norm_eq_of_oangle_eq_zero {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} (h : o.oangle x y = 0) :

Two vectors with zero angle between them are equal if and only if they have equal norms.

@[simp]
theorem orientation.oangle_add {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y z : V} (hx : x 0) (hy : y 0) (hz : z 0) :
o.oangle x y + o.oangle y z = o.oangle x z

Given three nonzero vectors, the angle between the first and the second plus the angle between the second and the third equals the angle between the first and the third.

@[simp]
theorem orientation.oangle_add_swap {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y z : V} (hx : x 0) (hy : y 0) (hz : z 0) :
o.oangle y z + o.oangle x y = o.oangle x z

Given three nonzero vectors, the angle between the second and the third plus the angle between the first and the second equals the angle between the first and the third.

@[simp]
theorem orientation.oangle_sub_left {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y z : V} (hx : x 0) (hy : y 0) (hz : z 0) :
o.oangle x z - o.oangle x y = o.oangle y z

Given three nonzero vectors, the angle between the first and the third minus the angle between the first and the second equals the angle between the second and the third.

@[simp]
theorem orientation.oangle_sub_right {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y z : V} (hx : x 0) (hy : y 0) (hz : z 0) :
o.oangle x z - o.oangle y z = o.oangle x y

Given three nonzero vectors, the angle between the first and the third minus the angle between the second and the third equals the angle between the first and the second.

@[simp]
theorem orientation.oangle_add_cyc3 {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y z : V} (hx : x 0) (hy : y 0) (hz : z 0) :
o.oangle x y + o.oangle y z + o.oangle z x = 0

Given three nonzero vectors, adding the angles between them in cyclic order results in 0.

@[simp]
theorem orientation.oangle_add_cyc3_neg_left {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y z : V} (hx : x 0) (hy : y 0) (hz : z 0) :
o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = real.pi

Given three nonzero vectors, adding the angles between them in cyclic order, with the first vector in each angle negated, results in π. If the vectors add to 0, this is a version of the sum of the angles of a triangle.

@[simp]
theorem orientation.oangle_add_cyc3_neg_right {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y z : V} (hx : x 0) (hy : y 0) (hz : z 0) :
o.oangle x (-y) + o.oangle y (-z) + o.oangle z (-x) = real.pi

Given three nonzero vectors, adding the angles between them in cyclic order, with the second vector in each angle negated, results in π. If the vectors add to 0, this is a version of the sum of the angles of a triangle.

theorem orientation.oangle_sub_eq_oangle_sub_rev_of_norm_eq {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} (h : x = y) :
o.oangle x (x - y) = o.oangle (y - x) y

Pons asinorum, oriented vector angle form.

theorem orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} (hn : x y) (h : x = y) :
o.oangle y x = real.pi - 2 o.oangle (y - x) y

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

theorem orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y z : V} (hxyne : x y) (hxzne : x z) (hxy : x = y) (hxz : x = z) :
o.oangle y z = 2 o.oangle (y - x) (z - x)

Angle at center of a circle equals twice angle at circumference, oriented vector angle form.

theorem orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y z : V} (hxyne : x y) (hxzne : x z) {r : } (hx : x = r) (hy : y = r) (hz : z = r) :
o.oangle y z = 2 o.oangle (y - x) (z - x)

Angle at center of a circle equals twice angle at circumference, oriented vector angle form with radius specified.

theorem orientation.two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x₁ x₂ y z : V} (hx₁yne : x₁ y) (hx₁zne : x₁ z) (hx₂yne : x₂ y) (hx₂zne : x₂ z) {r : } (hx₁ : x₁ = r) (hx₂ : x₂ = r) (hy : y = r) (hz : z = r) :
2 o.oangle (y - x₁) (z - x₁) = 2 o.oangle (y - x₂) (z - x₂)

Oriented vector angle version of "angles in same segment are equal" and "opposite angles of a cyclic quadrilateral add to π", for oriented angles mod π (for which those are the same result), represented here as equality of twice the angles.

noncomputable def orientation.rotation {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (θ : real.angle) :

A rotation by the oriented angle θ.

Equations
@[simp]

The determinant of rotation (as a linear map) is equal to 1.

@[simp]

The determinant of rotation (as a linear equiv) is equal to 1.

@[simp]
theorem orientation.rotation_symm {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (θ : real.angle) :
(o.rotation θ).symm = o.rotation (-θ)

The inverse of rotation is rotation by the negation of the angle.

@[simp]

Rotation by 0 is the identity.

Rotation by π is negation.

@[simp]
theorem orientation.rotation_trans {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (θ₁ θ₂ : real.angle) :
(o.rotation θ₁).trans (o.rotation θ₂) = o.rotation (θ₂ + θ₁)

Rotating twice is equivalent to rotating by the sum of the angles.

@[simp]
theorem orientation.oangle_rotation_left {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} (hx : x 0) (hy : y 0) (θ : real.angle) :
o.oangle ((o.rotation θ) x) y = o.oangle x y - θ

Rotating the first vector by θ subtracts θ from the angle between two vectors.

@[simp]
theorem orientation.oangle_rotation_right {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} (hx : x 0) (hy : y 0) (θ : real.angle) :
o.oangle x ((o.rotation θ) y) = o.oangle x y + θ

Rotating the second vector by θ adds θ to the angle between two vectors.

@[simp]
theorem orientation.oangle_rotation_self_left {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x : V} (hx : x 0) (θ : real.angle) :
o.oangle ((o.rotation θ) x) x = -θ

The rotation of a vector by θ has an angle of from that vector.

@[simp]
theorem orientation.oangle_rotation_self_right {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x : V} (hx : x 0) (θ : real.angle) :
o.oangle x ((o.rotation θ) x) = θ

A vector has an angle of θ from the rotation of that vector by θ.

@[simp]
theorem orientation.oangle_rotation_oangle_left {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) :
o.oangle ((o.rotation (o.oangle x y)) x) y = 0

Rotating the first vector by the angle between the two vectors results an an angle of 0.

@[simp]
theorem orientation.oangle_rotation_oangle_right {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) :
o.oangle y ((o.rotation (o.oangle x y)) x) = 0

Rotating the first vector by the angle between the two vectors and swapping the vectors results an an angle of 0.

@[simp]
theorem orientation.oangle_rotation {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) (θ : real.angle) :
o.oangle ((o.rotation θ) x) ((o.rotation θ) y) = o.oangle x y

Rotating both vectors by the same angle does not change the angle between those vectors.

@[simp]
theorem orientation.rotation_eq_self_iff_angle_eq_zero {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x : V} (hx : x 0) (θ : real.angle) :
(o.rotation θ) x = x θ = 0

A rotation of a nonzero vector equals that vector if and only if the angle is zero.

@[simp]
theorem orientation.eq_rotation_self_iff_angle_eq_zero {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x : V} (hx : x 0) (θ : real.angle) :
x = (o.rotation θ) x θ = 0

A nonzero vector equals a rotation of that vector if and only if the angle is zero.

theorem orientation.rotation_eq_self_iff {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x : V) (θ : real.angle) :
(o.rotation θ) x = x x = 0 θ = 0

A rotation of a vector equals that vector if and only if the vector or the angle is zero.

theorem orientation.eq_rotation_self_iff {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x : V) (θ : real.angle) :
x = (o.rotation θ) x x = 0 θ = 0

A vector equals a rotation of that vector if and only if the vector or the angle is zero.

@[simp]
theorem orientation.rotation_oangle_eq_iff_norm_eq {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) :
(o.rotation (o.oangle x y)) x = y x = y

Rotating a vector by the angle to another vector gives the second vector if and only if the norms are equal.

theorem orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} (hx : x 0) (hy : y 0) (θ : real.angle) :
o.oangle x y = θ y = (y / x) (o.rotation θ) x

The angle between two nonzero vectors is θ if and only if the second vector is the first rotated by θ and scaled by the ratio of the norms.

theorem orientation.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} (hx : x 0) (hy : y 0) (θ : real.angle) :
o.oangle x y = θ ∃ (r : ), 0 < r y = r (o.rotation θ) x

The angle between two nonzero vectors is θ if and only if the second vector is the first rotated by θ and scaled by a positive real.

theorem orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} (θ : real.angle) :
o.oangle x y = θ x 0 y 0 y = (y / x) (o.rotation θ) x θ = 0 (x = 0 y = 0)

The angle between two vectors is θ if and only if they are nonzero and the second vector is the first rotated by θ and scaled by the ratio of the norms, or θ and at least one of the vectors are zero.

theorem orientation.oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} (θ : real.angle) :
o.oangle x y = θ (x 0 y 0 ∃ (r : ), 0 < r y = r (o.rotation θ) x) θ = 0 (x = 0 y = 0)

The angle between two vectors is θ if and only if they are nonzero and the second vector is the first rotated by θ and scaled by a positive real, or θ and at least one of the vectors are zero.

Any linear isometric equivalence in V with positive determinant is rotation.

@[simp]
theorem orientation.oangle_map {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) (f : V ≃ₗᵢ[] V) :

The angle between two vectors, with respect to an orientation given by orientation.map with a linear isometric equivalence, equals the angle between those two vectors, transformed by the inverse of that equivalence, with respect to the original orientation.

theorem orientation.oangle_eq_basis_oangle {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {b : basis (fin 2) V} (hb : orthonormal b) (h : b.orientation = o) (x y : V) :
o.oangle x y = hb.oangle x y

orientation.oangle equals orthonormal.oangle for any orthonormal basis with that orientation.

theorem orientation.oangle_neg_orientation_eq_neg {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) (x y : V) :
(-o).oangle x y = -o.oangle x y

Negating the orientation negates the value of oangle.

theorem orientation.rotation_eq_basis_rotation {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {b : basis (fin 2) V} (hb : orthonormal b) (h : b.orientation = o) (θ : ) :

orientation.rotation equals orthonormal.rotation for any orthonormal basis with that orientation.

Negating the orientation negates the angle in rotation.

The inner product of two vectors is the product of the norms and the cosine of the oriented angle between the vectors.

theorem orientation.cos_oangle_eq_inner_div_norm_mul_norm {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} (hx : x 0) (hy : y 0) :

The cosine of the oriented angle between two nonzero vectors is the inner product divided by the product of the norms.

theorem orientation.cos_oangle_eq_cos_angle {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} (hx : x 0) (hy : y 0) :

The cosine of the oriented angle between two nonzero vectors equals that of the unoriented angle.

The oriented angle between two nonzero vectors is plus or minus the unoriented angle.

theorem orientation.angle_eq_abs_oangle_to_real {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} (hx : x 0) (hy : y 0) :

The unoriented angle between two nonzero vectors is the absolute value of the oriented angle, converted to a real.

If the sign of the oriented angle between two vectors is zero, either one of the vectors is zero or the unoriented angle is 0 or π.

theorem orientation.oangle_eq_of_angle_eq_of_sign_eq {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {w x y z : V} (h : inner_product_geometry.angle w x = inner_product_geometry.angle y z) (hs : (o.oangle w x).sign = (o.oangle y z).sign) :
o.oangle w x = o.oangle y z

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 orientation.oangle_eq_iff_angle_eq_of_sign_eq {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {w x y z : V} (hw : w 0) (hx : x 0) (hy : y 0) (hz : z 0) (hs : (o.oangle w x).sign = (o.oangle y z).sign) :

If the signs of two oriented angles between nonzero vectors are equal, the oriented angles are equal if and only if the unoriented angles are equal.

theorem orientation.oangle_eq_zero_iff_angle_eq_zero {V : Type u_1} [inner_product_space V] [hd2 : fact (finite_dimensional.finrank V = 2)] (o : orientation V (fin 2)) {x y : V} (hx : x 0) (hy : y 0) :

The oriented angle between two nonzero vectors is zero if and only if the unoriented angle is zero.

The oriented angle between two vectors is π if and only if the unoriented angle is π.