Oriented angles.

This file defines oriented angles in Euclidean affine spaces.

Main definitions

• EuclideanGeometry.oangle, with notation ∡, is the oriented angle determined by three points.

@[reducible, inline]

abbrev EuclideanGeometry.o {R : Type u_3} : {inst : StrictOrderedCommSemiring R} → {M : Type u_4} → {inst_1 : AddCommMonoid M} → {inst_2 : Module R M} → {ι : Type u_5} → [self : Module.Oriented R M ι] → Orientation R M ι

A fixed choice of positive orientation of Euclidean space ℝ²

Equations

• @EuclideanGeometry.o = @positiveOrientation

def EuclideanGeometry.oangle {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (p₁ : P) (p₂ : P) (p₃ : P) : Real.Angle

The oriented angle at p₂ between the line segments to p₁ and p₃, modulo 2 * π. If either of those points equals p₂, this is 0. See EuclideanGeometry.angle for the corresponding unoriented angle definition.

Equations

• EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)

def EuclideanGeometry.«term∡» : Lean.ParserDescr

The oriented angle at p₂ between the line segments to p₁ and p₃, modulo 2 * π. If either of those points equals p₂, this is 0. See EuclideanGeometry.angle for the corresponding unoriented angle definition.

Equations

• EuclideanGeometry.«term∡» = Lean.ParserDescr.node `EuclideanGeometry.«term∡» 1024 (Lean.ParserDescr.symbol "∡")

theorem EuclideanGeometry.continuousAt_oangle {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {x : P × P × P} (hx12 : x.1 ≠ x.2.1) (hx32 : x.2.2 ≠ x.2.1) : ContinuousAt (fun (y : P × P × P) => EuclideanGeometry.oangle y.1 y.2.1 y.2.2) x

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

@[simp]

theorem EuclideanGeometry.oangle_self_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (p₁ : P) (p₂ : P) : EuclideanGeometry.oangle p₁ p₁ p₂ = 0

The angle ∡AAB at a point.

@[simp]

theorem EuclideanGeometry.oangle_self_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (p₁ : P) (p₂ : P) : EuclideanGeometry.oangle p₁ p₂ p₂ = 0

The angle ∡ABB at a point.

@[simp]

theorem EuclideanGeometry.oangle_self_left_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (p₁ : P) (p₂ : P) : EuclideanGeometry.oangle p₁ p₂ p₁ = 0

The angle ∡ABA at a point.

theorem EuclideanGeometry.left_ne_of_oangle_ne_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ ≠ 0) : p₁ ≠ p₂

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

theorem EuclideanGeometry.right_ne_of_oangle_ne_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ ≠ 0) : p₃ ≠ p₂

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

theorem EuclideanGeometry.left_ne_right_of_oangle_ne_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ ≠ 0) : p₁ ≠ p₃

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

theorem EuclideanGeometry.left_ne_of_oangle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi) : p₁ ≠ p₂

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

theorem EuclideanGeometry.right_ne_of_oangle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi) : p₃ ≠ p₂

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

theorem EuclideanGeometry.left_ne_right_of_oangle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi) : p₁ ≠ p₃

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

theorem EuclideanGeometry.left_ne_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : p₁ ≠ p₂

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

theorem EuclideanGeometry.right_ne_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : p₃ ≠ p₂

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

theorem EuclideanGeometry.left_ne_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : p₁ ≠ p₃

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

theorem EuclideanGeometry.left_ne_of_oangle_eq_neg_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(-Real.pi / 2)) : p₁ ≠ p₂

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

theorem EuclideanGeometry.right_ne_of_oangle_eq_neg_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(-Real.pi / 2)) : p₃ ≠ p₂

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

theorem EuclideanGeometry.left_ne_right_of_oangle_eq_neg_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(-Real.pi / 2)) : p₁ ≠ p₃

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

theorem EuclideanGeometry.left_ne_of_oangle_sign_ne_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : (EuclideanGeometry.oangle p₁ p₂ p₃).sign ≠ 0) : p₁ ≠ p₂

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

theorem EuclideanGeometry.right_ne_of_oangle_sign_ne_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : (EuclideanGeometry.oangle p₁ p₂ p₃).sign ≠ 0) : p₃ ≠ p₂

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

theorem EuclideanGeometry.left_ne_right_of_oangle_sign_ne_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : (EuclideanGeometry.oangle p₁ p₂ p₃).sign ≠ 0) : p₁ ≠ p₃

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

theorem EuclideanGeometry.left_ne_of_oangle_sign_eq_one {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : (EuclideanGeometry.oangle p₁ p₂ p₃).sign = 1) : p₁ ≠ p₂

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

theorem EuclideanGeometry.right_ne_of_oangle_sign_eq_one {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : (EuclideanGeometry.oangle p₁ p₂ p₃).sign = 1) : p₃ ≠ p₂

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

theorem EuclideanGeometry.left_ne_right_of_oangle_sign_eq_one {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : (EuclideanGeometry.oangle p₁ p₂ p₃).sign = 1) : p₁ ≠ p₃

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

theorem EuclideanGeometry.left_ne_of_oangle_sign_eq_neg_one {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : (EuclideanGeometry.oangle p₁ p₂ p₃).sign = -1) : p₁ ≠ p₂

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

theorem EuclideanGeometry.right_ne_of_oangle_sign_eq_neg_one {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : (EuclideanGeometry.oangle p₁ p₂ p₃).sign = -1) : p₃ ≠ p₂

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

theorem EuclideanGeometry.left_ne_right_of_oangle_sign_eq_neg_one {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : (EuclideanGeometry.oangle p₁ p₂ p₃).sign = -1) : p₁ ≠ p₃

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

theorem EuclideanGeometry.oangle_rev {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (p₁ : P) (p₂ : P) (p₃ : P) : EuclideanGeometry.oangle p₃ p₂ p₁ = -EuclideanGeometry.oangle p₁ p₂ p₃

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

@[simp]

theorem EuclideanGeometry.oangle_add_oangle_rev {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (p₁ : P) (p₂ : P) (p₃ : P) : EuclideanGeometry.oangle p₁ p₂ p₃ + EuclideanGeometry.oangle p₃ p₂ p₁ = 0

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

theorem EuclideanGeometry.oangle_eq_zero_iff_oangle_rev_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} : EuclideanGeometry.oangle p₁ p₂ p₃ = 0 ↔ EuclideanGeometry.oangle p₃ p₂ p₁ = 0

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

theorem EuclideanGeometry.oangle_eq_pi_iff_oangle_rev_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi ↔ EuclideanGeometry.oangle p₃ p₂ p₁ = ↑Real.pi

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

theorem EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} : EuclideanGeometry.oangle p₁ p₂ p₃ ≠ 0 ∧ EuclideanGeometry.oangle p₁ p₂ p₃ ≠ ↑Real.pi ↔ AffineIndependent ℝ ![p₁, p₂, p₃]

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

theorem EuclideanGeometry.oangle_eq_zero_or_eq_pi_iff_collinear {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} : EuclideanGeometry.oangle p₁ p₂ p₃ = 0 ∨ EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi ↔ Collinear ℝ {p₁, p₂, p₃}

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

theorem EuclideanGeometry.oangle_sign_eq_zero_iff_collinear {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} : (EuclideanGeometry.oangle p₁ p₂ p₃).sign = 0 ↔ Collinear ℝ {p₁, p₂, p₃}

An oriented angle has a sign zero if and only if the three points are collinear.

theorem EuclideanGeometry.affineIndependent_iff_of_two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} {p₄ : P} {p₅ : P} {p₆ : P} (h : 2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₄ p₅ p₆) : AffineIndependent ℝ ![p₁, p₂, p₃] ↔ AffineIndependent ℝ ![p₄, p₅, p₆]

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

theorem EuclideanGeometry.collinear_iff_of_two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} {p₄ : P} {p₅ : P} {p₆ : P} (h : 2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₄ p₅ p₆) : Collinear ℝ {p₁, p₂, p₃} ↔ Collinear ℝ {p₄, p₅, p₆}

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

theorem EuclideanGeometry.two_zsmul_oangle_of_vectorSpan_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} {p₄ : P} {p₅ : P} {p₆ : P} (h₁₂₄₅ : vectorSpan ℝ {p₁, p₂} = vectorSpan ℝ {p₄, p₅}) (h₃₂₆₅ : vectorSpan ℝ {p₃, p₂} = vectorSpan ℝ {p₆, p₅}) : 2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₄ p₅ p₆

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

theorem EuclideanGeometry.two_zsmul_oangle_of_parallel {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} {p₄ : P} {p₅ : P} {p₆ : P} (h₁₂₄₅ : (affineSpan ℝ {p₁, p₂}).Parallel (affineSpan ℝ {p₄, p₅})) (h₃₂₆₅ : (affineSpan ℝ {p₃, p₂}).Parallel (affineSpan ℝ {p₆, p₅})) : 2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₄ p₅ p₆

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

@[simp]

theorem EuclideanGeometry.oangle_add {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p : P} {p₁ : P} {p₂ : P} {p₃ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) (hp₃ : p₃ ≠ p) : EuclideanGeometry.oangle p₁ p p₂ + EuclideanGeometry.oangle p₂ p p₃ = EuclideanGeometry.oangle p₁ p p₃

Given three points not equal to p, the angle between the first and the second at p plus the angle between the second and the third equals the angle between the first and the third.

@[simp]

theorem EuclideanGeometry.oangle_add_swap {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p : P} {p₁ : P} {p₂ : P} {p₃ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) (hp₃ : p₃ ≠ p) : EuclideanGeometry.oangle p₂ p p₃ + EuclideanGeometry.oangle p₁ p p₂ = EuclideanGeometry.oangle p₁ p p₃

Given three points not equal to p, the angle between the second and the third at p plus the angle between the first and the second equals the angle between the first and the third.

@[simp]

theorem EuclideanGeometry.oangle_sub_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p : P} {p₁ : P} {p₂ : P} {p₃ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) (hp₃ : p₃ ≠ p) : EuclideanGeometry.oangle p₁ p p₃ - EuclideanGeometry.oangle p₁ p p₂ = EuclideanGeometry.oangle p₂ p p₃

Given three points not equal to p, the angle between the first and the third at p minus the angle between the first and the second equals the angle between the second and the third.

@[simp]

theorem EuclideanGeometry.oangle_sub_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p : P} {p₁ : P} {p₂ : P} {p₃ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) (hp₃ : p₃ ≠ p) : EuclideanGeometry.oangle p₁ p p₃ - EuclideanGeometry.oangle p₂ p p₃ = EuclideanGeometry.oangle p₁ p p₂

Given three points not equal to p, the angle between the first and the third at p minus the angle between the second and the third equals the angle between the first and the second.

@[simp]

theorem EuclideanGeometry.oangle_add_cyc3 {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p : P} {p₁ : P} {p₂ : P} {p₃ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) (hp₃ : p₃ ≠ p) : EuclideanGeometry.oangle p₁ p p₂ + EuclideanGeometry.oangle p₂ p p₃ + EuclideanGeometry.oangle p₃ p p₁ = 0

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

theorem EuclideanGeometry.oangle_eq_oangle_of_dist_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : dist p₁ p₂ = dist p₁ p₃) : EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₂ p₃ p₁

Pons asinorum, oriented angle-at-point form.

theorem EuclideanGeometry.oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (hn : p₂ ≠ p₃) (h : dist p₁ p₂ = dist p₁ p₃) : EuclideanGeometry.oangle p₃ p₁ p₂ = ↑Real.pi - 2 • EuclideanGeometry.oangle p₁ p₂ p₃

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

theorem EuclideanGeometry.abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : dist p₁ p₂ = dist p₁ p₃) : |(EuclideanGeometry.oangle p₁ p₂ p₃).toReal| < Real.pi / 2

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

theorem EuclideanGeometry.abs_oangle_left_toReal_lt_pi_div_two_of_dist_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : dist p₁ p₂ = dist p₁ p₃) : |(EuclideanGeometry.oangle p₂ p₃ p₁).toReal| < Real.pi / 2

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

theorem EuclideanGeometry.cos_oangle_eq_cos_angle {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p : P} {p₁ : P} {p₂ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) : (EuclideanGeometry.oangle p₁ p p₂).cos = Real.cos (EuclideanGeometry.angle p₁ p p₂)

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

theorem EuclideanGeometry.oangle_eq_angle_or_eq_neg_angle {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p : P} {p₁ : P} {p₂ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) : EuclideanGeometry.oangle p₁ p p₂ = ↑(EuclideanGeometry.angle p₁ p p₂) ∨ EuclideanGeometry.oangle p₁ p p₂ = -↑(EuclideanGeometry.angle p₁ p p₂)

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

theorem EuclideanGeometry.angle_eq_abs_oangle_toReal {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p : P} {p₁ : P} {p₂ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) : EuclideanGeometry.angle p₁ p p₂ = |(EuclideanGeometry.oangle p₁ p p₂).toReal|

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

theorem EuclideanGeometry.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p : P} {p₁ : P} {p₂ : P} (h : (EuclideanGeometry.oangle p₁ p p₂).sign = 0) : p₁ = p ∨ p₂ = p ∨ EuclideanGeometry.angle p₁ p p₂ = 0 ∨ EuclideanGeometry.angle p₁ p p₂ = Real.pi

If the sign of the oriented angle at p between two points is zero, either one of the points equals p or the unoriented angle is 0 or π.

theorem EuclideanGeometry.oangle_eq_of_angle_eq_of_sign_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} {p₄ : P} {p₅ : P} {p₆ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₄ p₅ p₆) (hs : (EuclideanGeometry.oangle p₁ p₂ p₃).sign = (EuclideanGeometry.oangle p₄ p₅ p₆).sign) : EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₄ p₅ p₆

If two unoriented angles are equal, and the signs of the corresponding oriented angles are equal, then the oriented angles are equal (even in degenerate cases).

theorem EuclideanGeometry.angle_eq_iff_oangle_eq_of_sign_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} {p₄ : P} {p₅ : P} {p₆ : P} (hp₁ : p₁ ≠ p₂) (hp₃ : p₃ ≠ p₂) (hp₄ : p₄ ≠ p₅) (hp₆ : p₆ ≠ p₅) (hs : (EuclideanGeometry.oangle p₁ p₂ p₃).sign = (EuclideanGeometry.oangle p₄ p₅ p₆).sign) : EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₄ p₅ p₆ ↔ EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₄ p₅ p₆

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

theorem EuclideanGeometry.oangle_eq_angle_of_sign_eq_one {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : (EuclideanGeometry.oangle p₁ p₂ p₃).sign = 1) : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(EuclideanGeometry.angle p₁ p₂ p₃)

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

theorem EuclideanGeometry.oangle_eq_neg_angle_of_sign_eq_neg_one {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : (EuclideanGeometry.oangle p₁ p₂ p₃).sign = -1) : EuclideanGeometry.oangle p₁ p₂ p₃ = -↑(EuclideanGeometry.angle p₁ p₂ p₃)

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

theorem EuclideanGeometry.oangle_eq_zero_iff_angle_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p : P} {p₁ : P} {p₂ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) : EuclideanGeometry.oangle p₁ p p₂ = 0 ↔ EuclideanGeometry.angle p₁ p p₂ = 0

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

theorem EuclideanGeometry.oangle_eq_pi_iff_angle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi

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

theorem EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2

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

theorem EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : EuclideanGeometry.angle p₃ p₂ p₁ = Real.pi / 2

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

theorem EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_neg_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(-Real.pi / 2)) : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2

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

theorem EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_neg_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(-Real.pi / 2)) : EuclideanGeometry.angle p₃ p₂ p₁ = Real.pi / 2

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

theorem EuclideanGeometry.oangle_swap₁₂_sign {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (p₁ : P) (p₂ : P) (p₃ : P) : -(EuclideanGeometry.oangle p₁ p₂ p₃).sign = (EuclideanGeometry.oangle p₂ p₁ p₃).sign

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

theorem EuclideanGeometry.oangle_swap₁₃_sign {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (p₁ : P) (p₂ : P) (p₃ : P) : -(EuclideanGeometry.oangle p₁ p₂ p₃).sign = (EuclideanGeometry.oangle p₃ p₂ p₁).sign

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

theorem EuclideanGeometry.oangle_swap₂₃_sign {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (p₁ : P) (p₂ : P) (p₃ : P) : -(EuclideanGeometry.oangle p₁ p₂ p₃).sign = (EuclideanGeometry.oangle p₁ p₃ p₂).sign

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

theorem EuclideanGeometry.oangle_rotate_sign {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (p₁ : P) (p₂ : P) (p₃ : P) : (EuclideanGeometry.oangle p₂ p₃ p₁).sign = (EuclideanGeometry.oangle p₁ p₂ p₃).sign

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

theorem EuclideanGeometry.oangle_eq_pi_iff_sbtw {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi ↔ Sbtw ℝ p₁ p₂ p₃

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

theorem Sbtw.oangle₁₂₃_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi

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

theorem Sbtw.oangle₃₂₁_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : EuclideanGeometry.oangle p₃ p₂ p₁ = ↑Real.pi

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

theorem Wbtw.oangle₂₁₃_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) : EuclideanGeometry.oangle p₂ p₁ p₃ = 0

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

theorem Sbtw.oangle₂₁₃_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : EuclideanGeometry.oangle p₂ p₁ p₃ = 0

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

theorem Wbtw.oangle₃₁₂_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) : EuclideanGeometry.oangle p₃ p₁ p₂ = 0

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

theorem Sbtw.oangle₃₁₂_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : EuclideanGeometry.oangle p₃ p₁ p₂ = 0

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

theorem Wbtw.oangle₂₃₁_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) : EuclideanGeometry.oangle p₂ p₃ p₁ = 0

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

theorem Sbtw.oangle₂₃₁_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : EuclideanGeometry.oangle p₂ p₃ p₁ = 0

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

theorem Wbtw.oangle₁₃₂_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) : EuclideanGeometry.oangle p₁ p₃ p₂ = 0

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

theorem Sbtw.oangle₁₃₂_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : EuclideanGeometry.oangle p₁ p₃ p₂ = 0

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

theorem EuclideanGeometry.oangle_eq_zero_iff_wbtw {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} : EuclideanGeometry.oangle p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁

The oriented angle between three points is zero if and only if one of the first and third points is weakly between the other two.

theorem Wbtw.oangle_eq_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₁' : P} {p₂ : P} {p₃ : P} (h : Wbtw ℝ p₂ p₁ p₁') (hp₁p₂ : p₁ ≠ p₂) : EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁' p₂ p₃

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

theorem Sbtw.oangle_eq_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₁' : P} {p₂ : P} {p₃ : P} (h : Sbtw ℝ p₂ p₁ p₁') : EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁' p₂ p₃

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

theorem Wbtw.oangle_eq_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} {p₃' : P} (h : Wbtw ℝ p₂ p₃ p₃') (hp₃p₂ : p₃ ≠ p₂) : EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁ p₂ p₃'

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

theorem Sbtw.oangle_eq_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} {p₃' : P} (h : Sbtw ℝ p₂ p₃ p₃') : EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁ p₂ p₃'

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

@[simp]

theorem EuclideanGeometry.oangle_midpoint_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (p₁ : P) (p₂ : P) (p₃ : P) : EuclideanGeometry.oangle (midpoint ℝ p₁ p₂) p₂ p₃ = EuclideanGeometry.oangle p₁ p₂ p₃

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

@[simp]

theorem EuclideanGeometry.oangle_midpoint_rev_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (p₁ : P) (p₂ : P) (p₃ : P) : EuclideanGeometry.oangle (midpoint ℝ p₂ p₁) p₂ p₃ = EuclideanGeometry.oangle p₁ p₂ p₃

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

@[simp]

theorem EuclideanGeometry.oangle_midpoint_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (p₁ : P) (p₂ : P) (p₃ : P) : EuclideanGeometry.oangle p₁ p₂ (midpoint ℝ p₃ p₂) = EuclideanGeometry.oangle p₁ p₂ p₃

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

@[simp]

theorem EuclideanGeometry.oangle_midpoint_rev_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (p₁ : P) (p₂ : P) (p₃ : P) : EuclideanGeometry.oangle p₁ p₂ (midpoint ℝ p₂ p₃) = EuclideanGeometry.oangle p₁ p₂ p₃

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

theorem Sbtw.oangle_eq_add_pi_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₁' : P} {p₂ : P} {p₃ : P} (h : Sbtw ℝ p₁ p₂ p₁') (hp₃p₂ : p₃ ≠ p₂) : EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁' p₂ p₃ + ↑Real.pi

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

theorem Sbtw.oangle_eq_add_pi_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} {p₃' : P} (h : Sbtw ℝ p₃ p₂ p₃') (hp₁p₂ : p₁ ≠ p₂) : EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁ p₂ p₃' + ↑Real.pi

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

theorem Sbtw.oangle_eq_left_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₁' : P} {p₂ : P} {p₃ : P} {p₃' : P} (h₁ : Sbtw ℝ p₁ p₂ p₁') (h₃ : Sbtw ℝ p₃ p₂ p₃') : EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁' p₂ p₃'

Replacing both the first and third points by ones on the same lines but the opposite rays does not change the oriented angle (vertically opposite angles).

theorem Collinear.two_zsmul_oangle_eq_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₁' : P} {p₂ : P} {p₃ : P} (h : Collinear ℝ {p₁, p₂, p₁'}) (hp₁p₂ : p₁ ≠ p₂) (hp₁'p₂ : p₁' ≠ p₂) : 2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₁' p₂ p₃

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

theorem Collinear.two_zsmul_oangle_eq_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} {p₃' : P} (h : Collinear ℝ {p₃, p₂, p₃'}) (hp₃p₂ : p₃ ≠ p₂) (hp₃'p₂ : p₃' ≠ p₂) : 2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₁ p₂ p₃'

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

theorem EuclideanGeometry.dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p : P} (h : p₁ ≠ p₂) : dist p₁ p = dist p₂ p ↔ ∃ (r : ℝ), r • (EuclideanGeometry.o.rotation ↑(Real.pi / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p

Two different points are equidistant from a third point if and only if that third point equals some multiple of a π / 2 rotation of the vector between those points, plus the midpoint of those points.

theorem Collinear.oangle_sign_of_sameRay_vsub {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} {p₄ : P} (p₅ : P) (hp₁p₂ : p₁ ≠ p₂) (hp₃p₄ : p₃ ≠ p₄) (hc : Collinear ℝ {p₁, p₂, p₃, p₄}) (hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)) : (EuclideanGeometry.oangle p₁ p₅ p₂).sign = (EuclideanGeometry.oangle p₃ p₅ p₄).sign

Given two pairs of distinct points on the same line, such that the vectors between those pairs of points are on the same ray (oriented in the same direction on that line), and a fifth point, the angles at the fifth point between each of those two pairs of points have the same sign.

theorem Sbtw.oangle_sign_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (p₄ : P) (h : Sbtw ℝ p₁ p₂ p₃) : (EuclideanGeometry.oangle p₁ p₄ p₂).sign = (EuclideanGeometry.oangle p₂ p₄ p₃).sign

Given three points in strict order on the same line, and a fourth point, the angles at the fourth point between the first and second or second and third points have the same sign.

theorem Wbtw.oangle_sign_eq_of_ne_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (p₄ : P) (h : Wbtw ℝ p₁ p₂ p₃) (hne : p₁ ≠ p₂) : (EuclideanGeometry.oangle p₁ p₄ p₂).sign = (EuclideanGeometry.oangle p₁ p₄ p₃).sign

Given three points in weak order on the same line, with the first not equal to the second, and a fourth point, the angles at the fourth point between the first and second or first and third points have the same sign.

theorem Sbtw.oangle_sign_eq_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (p₄ : P) (h : Sbtw ℝ p₁ p₂ p₃) : (EuclideanGeometry.oangle p₁ p₄ p₂).sign = (EuclideanGeometry.oangle p₁ p₄ p₃).sign

Given three points in strict order on the same line, and a fourth point, the angles at the fourth point between the first and second or first and third points have the same sign.

theorem Wbtw.oangle_sign_eq_of_ne_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (p₄ : P) (h : Wbtw ℝ p₁ p₂ p₃) (hne : p₂ ≠ p₃) : (EuclideanGeometry.oangle p₂ p₄ p₃).sign = (EuclideanGeometry.oangle p₁ p₄ p₃).sign

Given three points in weak order on the same line, with the second not equal to the third, and a fourth point, the angles at the fourth point between the second and third or first and third points have the same sign.

theorem Sbtw.oangle_sign_eq_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (p₄ : P) (h : Sbtw ℝ p₁ p₂ p₃) : (EuclideanGeometry.oangle p₂ p₄ p₃).sign = (EuclideanGeometry.oangle p₁ p₄ p₃).sign

Given three points in strict order on the same line, and a fourth point, the angles at the fourth point between the second and third or first and third points have the same sign.

theorem AffineSubspace.SSameSide.oangle_sign_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : AffineSubspace ℝ P} {p₁ : P} {p₂ : P} {p₃ : P} {p₄ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃p₄ : s.SSameSide p₃ p₄) : (EuclideanGeometry.oangle p₁ p₄ p₂).sign = (EuclideanGeometry.oangle p₁ p₃ p₂).sign

Given two points in an affine subspace, the angles between those two points at two other points on the same side of that subspace have the same sign.

theorem AffineSubspace.SOppSide.oangle_sign_eq_neg {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : AffineSubspace ℝ P} {p₁ : P} {p₂ : P} {p₃ : P} {p₄ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃p₄ : s.SOppSide p₃ p₄) : (EuclideanGeometry.oangle p₁ p₄ p₂).sign = -(EuclideanGeometry.oangle p₁ p₃ p₂).sign

Given two points in an affine subspace, the angles between those two points at two other points on opposite sides of that subspace have opposite signs.