Angles in circles and sphere.

This file proves results about angles in circles and spheres.

theorem Orientation.oangle_eq_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} {z : V} (hxyne : x ≠ y) (hxzne : x ≠ z) (hxy : ‖x‖ = ‖y‖) (hxz : ‖x‖ = ‖z‖) : Orientation.oangle o y z = 2 • Orientation.oangle o (y - x) (z - x)

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

theorem Orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} {z : V} (hxyne : x ≠ y) (hxzne : x ≠ z) {r : ℝ} (hx : ‖x‖ = r) (hy : ‖y‖ = r) (hz : ‖z‖ = r) : Orientation.oangle o y z = 2 • Orientation.oangle o (y - x) (z - x)

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

theorem Orientation.two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x₁ : V} {x₂ : V} {y : V} {z : V} (hx₁yne : x₁ ≠ y) (hx₁zne : x₁ ≠ z) (hx₂yne : x₂ ≠ y) (hx₂zne : x₂ ≠ z) {r : ℝ} (hx₁ : ‖x₁‖ = r) (hx₂ : ‖x₂‖ = r) (hy : ‖y‖ = r) (hz : ‖z‖ = r) : 2 • Orientation.oangle o (y - x₁) (z - x₁) = 2 • Orientation.oangle o (y - x₂) (z - x₂)

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

theorem EuclideanGeometry.Sphere.oangle_center_eq_two_zsmul_oangle {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} {p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₃ : p₂ ≠ p₃) : EuclideanGeometry.oangle p₁ s.center p₃ = 2 • EuclideanGeometry.oangle p₁ p₂ p₃

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

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

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

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

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

theorem EuclideanGeometry.Sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) : EuclideanGeometry.oangle p₁ s.center p₂ = ↑Real.pi - 2 • EuclideanGeometry.oangle s.center p₂ p₁

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

theorem EuclideanGeometry.Sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) : EuclideanGeometry.oangle p₁ s.center p₂ = ↑Real.pi - 2 • EuclideanGeometry.oangle p₂ p₁ s.center

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

theorem EuclideanGeometry.Sphere.two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} {p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₃ : p₂ ≠ p₃) (hp₁p₃ : p₁ ≠ p₃) : 2 • EuclideanGeometry.oangle p₃ p₁ s.center + 2 • EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi

Twice a base angle of an isosceles triangle with apex at the center of a circle, plus twice the angle at the apex of a triangle with the same base but apex on the circle, equals π.

theorem EuclideanGeometry.Sphere.abs_oangle_center_left_toReal_lt_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) : |Real.Angle.toReal (EuclideanGeometry.oangle s.center p₂ p₁)| < Real.pi / 2

A base angle of an isosceles triangle with apex at the center of a circle is acute.

theorem EuclideanGeometry.Sphere.abs_oangle_center_right_toReal_lt_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) : |Real.Angle.toReal (EuclideanGeometry.oangle p₂ p₁ s.center)| < Real.pi / 2

A base angle of an isosceles triangle with apex at the center of a circle is acute.

theorem EuclideanGeometry.Sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) : (Real.Angle.tan (EuclideanGeometry.oangle p₂ p₁ s.center) / 2) • (Orientation.rotation EuclideanGeometry.o ↑(Real.pi / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center

Given two points on a circle, the center of that circle may be expressed explicitly as a multiple (by half the tangent of the angle between the chord and the radius at one of those points) of a π / 2 rotation of the vector between those points, plus the midpoint of those points.

theorem EuclideanGeometry.Sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} {p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₁p₂ : p₁ ≠ p₂) (hp₁p₃ : p₁ ≠ p₃) (hp₂p₃ : p₂ ≠ p₃) : ((Real.Angle.tan (EuclideanGeometry.oangle p₁ p₂ p₃))⁻¹ / 2) • (Orientation.rotation EuclideanGeometry.o ↑(Real.pi / 2)) (p₃ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₃ = s.center

Given three points on a circle, the center of that circle may be expressed explicitly as a multiple (by half the inverse of the tangent of the angle at one of those points) of a π / 2 rotation of the vector between the other two points, plus the midpoint of those points.

theorem EuclideanGeometry.Sphere.dist_div_cos_oangle_center_div_two_eq_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) : dist p₁ p₂ / Real.Angle.cos (EuclideanGeometry.oangle p₂ p₁ s.center) / 2 = s.radius

Given two points on a circle, the radius of that circle may be expressed explicitly as half the distance between those two points divided by the cosine of the angle between the chord and the radius at one of those points.

theorem EuclideanGeometry.Sphere.dist_div_cos_oangle_center_eq_two_mul_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) : dist p₁ p₂ / Real.Angle.cos (EuclideanGeometry.oangle p₂ p₁ s.center) = 2 * s.radius

Given two points on a circle, twice the radius of that circle may be expressed explicitly as the distance between those two points divided by the cosine of the angle between the chord and the radius at one of those points.

theorem EuclideanGeometry.Sphere.dist_div_sin_oangle_div_two_eq_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} {p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₁p₂ : p₁ ≠ p₂) (hp₁p₃ : p₁ ≠ p₃) (hp₂p₃ : p₂ ≠ p₃) : dist p₁ p₃ / |Real.Angle.sin (EuclideanGeometry.oangle p₁ p₂ p₃)| / 2 = s.radius

Given three points on a circle, the radius of that circle may be expressed explicitly as half the distance between two of those points divided by the absolute value of the sine of the angle at the third point (a version of the law of sines or sine rule).

theorem EuclideanGeometry.Sphere.dist_div_sin_oangle_eq_two_mul_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} {p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₁p₂ : p₁ ≠ p₂) (hp₁p₃ : p₁ ≠ p₃) (hp₂p₃ : p₂ ≠ p₃) : dist p₁ p₃ / |Real.Angle.sin (EuclideanGeometry.oangle p₁ p₂ p₃)| = 2 * s.radius

Given three points on a circle, twice the radius of that circle may be expressed explicitly as the distance between two of those points divided by the absolute value of the sine of the angle at the third point (a version of the law of sines or sine rule).

theorem Affine.Triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Affine.Triangle ℝ P) {i₁ : Fin 3} {i₂ : Fin 3} {i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : ((Real.Angle.tan (EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)))⁻¹ / 2) • (Orientation.rotation EuclideanGeometry.o ↑(Real.pi / 2)) (t.points i₃ -ᵥ t.points i₁) +ᵥ midpoint ℝ (t.points i₁) (t.points i₃) = Affine.Simplex.circumcenter t

The circumcenter of a triangle may be expressed explicitly as a multiple (by half the inverse of the tangent of the angle at one of the vertices) of a π / 2 rotation of the vector between the other two vertices, plus the midpoint of those vertices.

theorem Affine.Triangle.dist_div_sin_oangle_div_two_eq_circumradius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Affine.Triangle ℝ P) {i₁ : Fin 3} {i₂ : Fin 3} {i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : dist (t.points i₁) (t.points i₃) / |Real.Angle.sin (EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃))| / 2 = Affine.Simplex.circumradius t

The circumradius of a triangle may be expressed explicitly as half the length of a side divided by the absolute value of the sine of the angle at the third point (a version of the law of sines or sine rule).

theorem Affine.Triangle.dist_div_sin_oangle_eq_two_mul_circumradius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Affine.Triangle ℝ P) {i₁ : Fin 3} {i₂ : Fin 3} {i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : dist (t.points i₁) (t.points i₃) / |Real.Angle.sin (EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃))| = 2 * Affine.Simplex.circumradius t

Twice the circumradius of a triangle may be expressed explicitly as the length of a side divided by the absolute value of the sine of the angle at the third point (a version of the law of sines or sine rule).

theorem Affine.Triangle.circumsphere_eq_of_dist_of_oangle {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Affine.Triangle ℝ P) {i₁ : Fin 3} {i₂ : Fin 3} {i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : Affine.Simplex.circumsphere t = { center := ((Real.Angle.tan (EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)))⁻¹ / 2) • (Orientation.rotation EuclideanGeometry.o ↑(Real.pi / 2)) (t.points i₃ -ᵥ t.points i₁) +ᵥ midpoint ℝ (t.points i₁) (t.points i₃), radius := dist (t.points i₁) (t.points i₃) / |Real.Angle.sin (EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃))| / 2 }

The circumsphere of a triangle may be expressed explicitly in terms of two points and the angle at the third point.

theorem Affine.Triangle.circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {t₁ : Affine.Triangle ℝ P} {t₂ : Affine.Triangle ℝ P} {i₁ : Fin 3} {i₂ : Fin 3} {i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) (h₁ : t₁.points i₁ = t₂.points i₁) (h₃ : t₁.points i₃ = t₂.points i₃) (h₂ : 2 • EuclideanGeometry.oangle (t₁.points i₁) (t₁.points i₂) (t₁.points i₃) = 2 • EuclideanGeometry.oangle (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)) : Affine.Simplex.circumsphere t₁ = Affine.Simplex.circumsphere t₂

If two triangles have two points the same, and twice the angle at the third point the same, they have the same circumsphere.

theorem Affine.Triangle.mem_circumsphere_of_two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {t : Affine.Triangle ℝ P} {p : P} {i₁ : Fin 3} {i₂ : Fin 3} {i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) (h : 2 • EuclideanGeometry.oangle (t.points i₁) p (t.points i₃) = 2 • EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)) : p ∈ Affine.Simplex.circumsphere t

Given a triangle, and a fourth point such that twice the angle between two points of the triangle at that fourth point equals twice the third angle of the triangle, the fourth point lies in the circumsphere of the triangle.

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

Converse of "angles in same segment are equal" and "opposite angles of a cyclic quadrilateral add to π", for oriented angles mod π.

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

Converse of "angles in same segment are equal" and "opposite angles of a cyclic quadrilateral add to π", for oriented angles mod π, with a "concyclic" conclusion.

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

Converse of "angles in same segment are equal" and "opposite angles of a cyclic quadrilateral add to π", for oriented angles mod π, with a "cospherical or collinear" conclusion.

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

Converse of "angles in same segment are equal" and "opposite angles of a cyclic quadrilateral add to π", for oriented angles mod π, with a "concyclic or collinear" conclusion.