Oriented angles.

This file defines oriented angles in real inner product spaces.

Main definitions

• Orientation.oangle is the oriented angle between two vectors with respect to an orientation.

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 : ℤ) • θ.

References

• Evan Chen, Euclidean Geometry in Mathematical Olympiads.

def Orientation.oangle {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) : Real.Angle

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

Equations

• o.oangle x y = ↑((o.kahler x) y).arg

theorem Orientation.continuousAt_oangle {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V × V} (hx1 : x.1 ≠ 0) (hx2 : x.2 ≠ 0) : ContinuousAt (fun (y : V × V) => o.oangle y.1 y.2) x

Oriented angles are continuous when the vectors involved are nonzero.

@[simp]

theorem Orientation.oangle_zero_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.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.left_ne_zero_of_oangle_ne_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : o.oangle x y ≠ 0) : x ≠ 0

If the angle between two vectors is nonzero, the first vector is nonzero.

theorem Orientation.right_ne_zero_of_oangle_ne_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : o.oangle x y ≠ 0) : y ≠ 0

If the angle between two vectors is nonzero, the second vector is nonzero.

theorem Orientation.ne_of_oangle_ne_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : o.oangle x y ≠ 0) : x ≠ y

If the angle between two vectors is nonzero, the vectors are not equal.

theorem Orientation.left_ne_zero_of_oangle_eq_pi {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : o.oangle x y = ↑Real.pi) : x ≠ 0

If the angle between two vectors is π, the first vector is nonzero.

theorem Orientation.right_ne_zero_of_oangle_eq_pi {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : o.oangle x y = ↑Real.pi) : y ≠ 0

If the angle between two vectors is π, the second vector is nonzero.

theorem Orientation.ne_of_oangle_eq_pi {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : o.oangle x y = ↑Real.pi) : x ≠ y

If the angle between two vectors is π, the vectors are not equal.

theorem Orientation.left_ne_zero_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : o.oangle x y = ↑(Real.pi / 2)) : x ≠ 0

If the angle between two vectors is π / 2, the first vector is nonzero.

theorem Orientation.right_ne_zero_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : o.oangle x y = ↑(Real.pi / 2)) : y ≠ 0

If the angle between two vectors is π / 2, the second vector is nonzero.

theorem Orientation.ne_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : o.oangle x y = ↑(Real.pi / 2)) : x ≠ y

If the angle between two vectors is π / 2, the vectors are not equal.

theorem Orientation.left_ne_zero_of_oangle_eq_neg_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : o.oangle x y = ↑(-Real.pi / 2)) : x ≠ 0

If the angle between two vectors is -π / 2, the first vector is nonzero.

theorem Orientation.right_ne_zero_of_oangle_eq_neg_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : o.oangle x y = ↑(-Real.pi / 2)) : y ≠ 0

If the angle between two vectors is -π / 2, the second vector is nonzero.

theorem Orientation.ne_of_oangle_eq_neg_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : o.oangle x y = ↑(-Real.pi / 2)) : x ≠ y

If the angle between two vectors is -π / 2, the vectors are not equal.

theorem Orientation.left_ne_zero_of_oangle_sign_ne_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : (o.oangle x y).sign ≠ 0) : x ≠ 0

If the sign of the angle between two vectors is nonzero, the first vector is nonzero.

theorem Orientation.right_ne_zero_of_oangle_sign_ne_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : (o.oangle x y).sign ≠ 0) : y ≠ 0

If the sign of the angle between two vectors is nonzero, the second vector is nonzero.

theorem Orientation.ne_of_oangle_sign_ne_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : (o.oangle x y).sign ≠ 0) : x ≠ y

If the sign of the angle between two vectors is nonzero, the vectors are not equal.

theorem Orientation.left_ne_zero_of_oangle_sign_eq_one {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : (o.oangle x y).sign = 1) : x ≠ 0

If the sign of the angle between two vectors is positive, the first vector is nonzero.

theorem Orientation.right_ne_zero_of_oangle_sign_eq_one {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : (o.oangle x y).sign = 1) : y ≠ 0

If the sign of the angle between two vectors is positive, the second vector is nonzero.

theorem Orientation.ne_of_oangle_sign_eq_one {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : (o.oangle x y).sign = 1) : x ≠ y

If the sign of the angle between two vectors is positive, the vectors are not equal.

theorem Orientation.left_ne_zero_of_oangle_sign_eq_neg_one {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : (o.oangle x y).sign = -1) : x ≠ 0

If the sign of the angle between two vectors is negative, the first vector is nonzero.

theorem Orientation.right_ne_zero_of_oangle_sign_eq_neg_one {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : (o.oangle x y).sign = -1) : y ≠ 0

If the sign of the angle between two vectors is negative, the second vector is nonzero.

theorem Orientation.ne_of_oangle_sign_eq_neg_one {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : (o.oangle x y).sign = -1) : x ≠ y

If the sign of the angle between two vectors is negative, the vectors are not equal.

theorem Orientation.oangle_rev {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} (hx : x ≠ 0) : o.oangle (-x) x = ↑Real.pi

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

@[simp]

theorem Orientation.oangle_neg_self_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} (hx : x ≠ 0) : o.oangle x (-x) = ↑Real.pi

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

theorem Orientation.two_zsmul_oangle_neg_self_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.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.

theorem Orientation.two_zsmul_oangle_neg_self_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.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.two_zsmul_oangle_left_of_span_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (z : V) (h : Submodule.span ℝ {x} = Submodule.span ℝ {y}) : 2 • o.oangle x z = 2 • o.oangle y z

If the spans of two vectors are equal, twice angles with those vectors on the left are equal.

theorem Orientation.two_zsmul_oangle_right_of_span_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) {y : V} {z : V} (h : Submodule.span ℝ {y} = Submodule.span ℝ {z}) : 2 • o.oangle x y = 2 • o.oangle x z

If the spans of two vectors are equal, twice angles with those vectors on the right are equal.

theorem Orientation.two_zsmul_oangle_of_span_eq_of_span_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {w : V} {x : V} {y : V} {z : V} (hwx : Submodule.span ℝ {w} = Submodule.span ℝ {x}) (hyz : Submodule.span ℝ {y} = Submodule.span ℝ {z}) : 2 • o.oangle w y = 2 • o.oangle x z

If the spans of two pairs of vectors are equal, twice angles between those vectors are equal.

theorem Orientation.oangle_eq_zero_iff_oangle_rev_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {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_sameRay {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} : o.oangle x y = 0 ↔ SameRay ℝ x y

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

theorem Orientation.oangle_eq_pi_iff_oangle_rev_eq_pi {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} : o.oangle x y = ↑Real.pi ↔ o.oangle y x = ↑Real.pi

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

theorem Orientation.oangle_eq_pi_iff_sameRay_neg {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} : o.oangle x y = ↑Real.pi ↔ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ 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.

theorem Orientation.oangle_eq_zero_or_eq_pi_iff_not_linearIndependent {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} : o.oangle x y = 0 ∨ o.oangle x y = ↑Real.pi ↔ ¬LinearIndependent ℝ ![x, y]

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {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.

theorem Orientation.oangle_ne_zero_and_ne_pi_iff_linearIndependent {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} : o.oangle x y ≠ 0 ∧ o.oangle x y ≠ ↑Real.pi ↔ LinearIndependent ℝ ![x, y]

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : o.oangle x y = 0) : x = y ↔ ‖x‖ = ‖y‖

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} {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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} {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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} {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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} {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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} {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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} {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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} {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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {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.

@[simp]

theorem Orientation.oangle_map {V : Type u_1} {V' : Type u_2} [NormedAddCommGroup V] [NormedAddCommGroup V'] [InnerProductSpace ℝ V] [InnerProductSpace ℝ V'] [Fact (FiniteDimensional.finrank ℝ V = 2)] [Fact (FiniteDimensional.finrank ℝ V' = 2)] (o : Orientation ℝ V (Fin 2)) (x : V') (y : V') (f : V ≃ₗᵢ[ℝ] V') : ((Orientation.map (Fin 2) f.toLinearEquiv) o).oangle x y = o.oangle (f.symm x) (f.symm y)

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.

@[simp]

theorem Complex.oangle (w : ℂ) (z : ℂ) : Complex.orientation.oangle w z = ↑((starRingEnd ℂ) w * z).arg

theorem Orientation.oangle_map_complex {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (f : V ≃ₗᵢ[ℝ] ℂ) (hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation) (x : V) (y : V) : o.oangle x y = ↑((starRingEnd ℂ) (f x) * f y).arg

The oriented angle on an oriented real inner product space of dimension 2 can be evaluated in terms of a complex-number representation of the space.

theorem Orientation.oangle_neg_orientation_eq_neg {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) : (-o).oangle x y = -o.oangle x y

Negating the orientation negates the value of oangle.

theorem Orientation.inner_eq_norm_mul_norm_mul_cos_oangle {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) : ⟪x, y⟫_ℝ = ‖x‖ * ‖y‖ * (o.oangle x y).cos

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (hx : x ≠ 0) (hy : y ≠ 0) : (o.oangle x y).cos = ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (hx : x ≠ 0) (hy : y ≠ 0) : (o.oangle x y).cos = Real.cos (InnerProductGeometry.angle x y)

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

theorem Orientation.oangle_eq_angle_or_eq_neg_angle {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (hx : x ≠ 0) (hy : y ≠ 0) : o.oangle x y = ↑(InnerProductGeometry.angle x y) ∨ o.oangle x y = -↑(InnerProductGeometry.angle x y)

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

theorem Orientation.angle_eq_abs_oangle_toReal {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (hx : x ≠ 0) (hy : y ≠ 0) : InnerProductGeometry.angle x y = |(o.oangle x y).toReal|

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

theorem Orientation.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : (o.oangle x y).sign = 0) : x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = Real.pi

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {w : V} {x : V} {y : V} {z : V} (h : InnerProductGeometry.angle w x = InnerProductGeometry.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.angle_eq_iff_oangle_eq_of_sign_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {w : V} {x : V} {y : V} {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) : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = o.oangle y z

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_angle_of_sign_eq_one {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : (o.oangle x y).sign = 1) : o.oangle x y = ↑(InnerProductGeometry.angle x y)

The oriented angle between two vectors equals the unoriented angle if the sign is positive.

theorem Orientation.oangle_eq_neg_angle_of_sign_eq_neg_one {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : (o.oangle x y).sign = -1) : o.oangle x y = -↑(InnerProductGeometry.angle x y)

The oriented angle between two vectors equals minus the unoriented angle if the sign is negative.

theorem Orientation.oangle_eq_zero_iff_angle_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (hx : x ≠ 0) (hy : y ≠ 0) : o.oangle x y = 0 ↔ InnerProductGeometry.angle x y = 0

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

theorem Orientation.oangle_eq_pi_iff_angle_eq_pi {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} : o.oangle x y = ↑Real.pi ↔ InnerProductGeometry.angle x y = Real.pi

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

theorem Orientation.eq_zero_or_oangle_eq_iff_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} : x = 0 ∨ y = 0 ∨ o.oangle x y = ↑(Real.pi / 2) ∨ o.oangle x y = ↑(-Real.pi / 2) ↔ ⟪x, y⟫_ℝ = 0

One of two vectors is zero or the oriented angle between them is plus or minus π / 2 if and only if the inner product of those vectors is zero.

theorem Orientation.inner_eq_zero_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : o.oangle x y = ↑(Real.pi / 2)) : ⟪x, y⟫_ℝ = 0

If the oriented angle between two vectors is π / 2, the inner product of those vectors is zero.

theorem Orientation.inner_rev_eq_zero_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : o.oangle x y = ↑(Real.pi / 2)) : ⟪y, x⟫_ℝ = 0

If the oriented angle between two vectors is π / 2, the inner product of those vectors (reversed) is zero.

theorem Orientation.inner_eq_zero_of_oangle_eq_neg_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : o.oangle x y = ↑(-Real.pi / 2)) : ⟪x, y⟫_ℝ = 0

If the oriented angle between two vectors is -π / 2, the inner product of those vectors is zero.

theorem Orientation.inner_rev_eq_zero_of_oangle_eq_neg_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : o.oangle x y = ↑(-Real.pi / 2)) : ⟪y, x⟫_ℝ = 0

If the oriented angle between two vectors is -π / 2, the inner product of those vectors (reversed) is zero.

@[simp]

theorem Orientation.oangle_sign_neg_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) : (o.oangle (-x) y).sign = -(o.oangle x y).sign

Negating the first vector passed to oangle negates the sign of the angle.

@[simp]

theorem Orientation.oangle_sign_neg_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) : (o.oangle x (-y)).sign = -(o.oangle x y).sign

Negating the second vector passed to oangle negates the sign of the angle.

@[simp]

theorem Orientation.oangle_sign_smul_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) (r : ℝ) : (o.oangle (r • x) y).sign = SignType.sign r * (o.oangle x y).sign

Multiplying the first vector passed to oangle by a real multiplies the sign of the angle by the sign of the real.

@[simp]

theorem Orientation.oangle_sign_smul_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) (r : ℝ) : (o.oangle x (r • y)).sign = SignType.sign r * (o.oangle x y).sign

Multiplying the second vector passed to oangle by a real multiplies the sign of the angle by the sign of the real.

theorem Orientation.oangle_smul_add_right_eq_zero_or_eq_pi_iff {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (r : ℝ) : o.oangle x (r • x + y) = 0 ∨ o.oangle x (r • x + y) = ↑Real.pi ↔ o.oangle x y = 0 ∨ o.oangle x y = ↑Real.pi

Auxiliary lemma for the proof of oangle_sign_smul_add_right; not intended to be used outside of that proof.

@[simp]

theorem Orientation.oangle_sign_smul_add_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) (r : ℝ) : (o.oangle x (r • x + y)).sign = (o.oangle x y).sign

Adding a multiple of the first vector passed to oangle to the second vector does not change the sign of the angle.

@[simp]

theorem Orientation.oangle_sign_add_smul_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) (r : ℝ) : (o.oangle (x + r • y) y).sign = (o.oangle x y).sign

Adding a multiple of the second vector passed to oangle to the first vector does not change the sign of the angle.

@[simp]

theorem Orientation.oangle_sign_sub_smul_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) (r : ℝ) : (o.oangle x (y - r • x)).sign = (o.oangle x y).sign

Subtracting a multiple of the first vector passed to oangle from the second vector does not change the sign of the angle.

@[simp]

theorem Orientation.oangle_sign_sub_smul_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) (r : ℝ) : (o.oangle (x - r • y) y).sign = (o.oangle x y).sign

Subtracting a multiple of the second vector passed to oangle from the first vector does not change the sign of the angle.

@[simp]

theorem Orientation.oangle_sign_add_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) : (o.oangle x (x + y)).sign = (o.oangle x y).sign

Adding the first vector passed to oangle to the second vector does not change the sign of the angle.

@[simp]

theorem Orientation.oangle_sign_add_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) : (o.oangle (x + y) y).sign = (o.oangle x y).sign

Adding the second vector passed to oangle to the first vector does not change the sign of the angle.

@[simp]

theorem Orientation.oangle_sign_sub_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) : (o.oangle x (y - x)).sign = (o.oangle x y).sign

Subtracting the first vector passed to oangle from the second vector does not change the sign of the angle.

@[simp]

theorem Orientation.oangle_sign_sub_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) : (o.oangle (x - y) y).sign = (o.oangle x y).sign

Subtracting the second vector passed to oangle from the first vector does not change the sign of the angle.

@[simp]

theorem Orientation.oangle_sign_smul_sub_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) (r : ℝ) : (o.oangle x (r • x - y)).sign = -(o.oangle x y).sign

Subtracting the second vector passed to oangle from a multiple of the first vector negates the sign of the angle.

@[simp]

theorem Orientation.oangle_sign_smul_sub_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) (r : ℝ) : (o.oangle (r • y - x) y).sign = -(o.oangle x y).sign

Subtracting the first vector passed to oangle from a multiple of the second vector negates the sign of the angle.

theorem Orientation.oangle_sign_sub_right_eq_neg {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) : (o.oangle x (x - y)).sign = -(o.oangle x y).sign

Subtracting the second vector passed to oangle from the first vector negates the sign of the angle.

theorem Orientation.oangle_sign_sub_left_eq_neg {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) : (o.oangle (y - x) y).sign = -(o.oangle x y).sign

Subtracting the first vector passed to oangle from the second vector negates the sign of the angle.

@[simp]

theorem Orientation.oangle_sign_sub_right_swap {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) : (o.oangle y (y - x)).sign = (o.oangle x y).sign

Subtracting the first vector passed to oangle from the second vector then swapping the vectors does not change the sign of the angle.

@[simp]

theorem Orientation.oangle_sign_sub_left_swap {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) : (o.oangle (x - y) x).sign = (o.oangle x y).sign

Subtracting the second vector passed to oangle from the first vector then swapping the vectors does not change the sign of the angle.

theorem Orientation.oangle_sign_smul_add_smul_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) (r₁ : ℝ) (r₂ : ℝ) : (o.oangle x (r₁ • x + r₂ • y)).sign = SignType.sign r₂ * (o.oangle x y).sign

The sign of the angle between a vector, and a linear combination of that vector with a second vector, is the sign of the factor by which the second vector is multiplied in that combination multiplied by the sign of the angle between the two vectors.

theorem Orientation.oangle_sign_smul_add_smul_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) (r₁ : ℝ) (r₂ : ℝ) : (o.oangle (r₁ • x + r₂ • y) y).sign = SignType.sign r₁ * (o.oangle x y).sign

The sign of the angle between a linear combination of two vectors and the second vector is the sign of the factor by which the first vector is multiplied in that combination multiplied by the sign of the angle between the two vectors.

theorem Orientation.oangle_sign_smul_add_smul_smul_add_smul {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) (r₁ : ℝ) (r₂ : ℝ) (r₃ : ℝ) (r₄ : ℝ) : (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign

The sign of the angle between two linear combinations of two vectors is the sign of the determinant of the factors in those combinations multiplied by the sign of the angle between the two vectors.

theorem Orientation.abs_oangle_sub_left_toReal_lt_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : ‖x‖ = ‖y‖) : |(o.oangle (y - x) y).toReal| < Real.pi / 2

A base angle of an isosceles triangle is acute, oriented vector angle form.

theorem Orientation.abs_oangle_sub_right_toReal_lt_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : ‖x‖ = ‖y‖) : |(o.oangle x (x - y)).toReal| < Real.pi / 2

A base angle of an isosceles triangle is acute, oriented vector angle form.