Angles in circles and spheres

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

The angle at the center of a circle equals twice the angle at the 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 (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y z : V} (hxyne : x ≠ y) (hxzne : x ≠ z) {r : ℝ} (hx : ‖x‖ = r) (hy : ‖y‖ = r) (hz : ‖z‖ = r) : o.oangle y z = 2 • o.oangle (y - x) (z - x)

The angle at the center of a circle equals twice the angle at the circumference, oriented vector angle form with the 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 (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x₁ x₂ y z : V} (hx₁yne : x₁ ≠ y) (hx₁zne : x₁ ≠ z) (hx₂yne : x₂ ≠ y) (hx₂zne : x₂ ≠ z) {r : ℝ} (hx₁ : ‖x₁‖ = r) (hx₂ : ‖x₂‖ = r) (hy : ‖y‖ = r) (hz : ‖z‖ = r) : 2 • o.oangle (y - x₁) (z - x₁) = 2 • o.oangle (y - x₂) (z - x₂)

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

theorem EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} {s : Sphere P} (hd : s.IsDiameter p₁ p₃) : angle p₁ p₂ p₃ = Real.pi / 2 ↔ p₂ ∈ s

Thales' theorem: The angle inscribed in a semicircle is a right angle.

theorem EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_ofDiameter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} : angle p₁ p₂ p₃ = Real.pi / 2 ↔ p₂ ∈ Sphere.ofDiameter p₁ p₃

Thales' theorem: For three distinct points, the angle at the second point is a right angle if and only if the second point lies on the sphere having the first and third points as diameter endpoints.

theorem EuclideanGeometry.Sphere.thales_theorem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} {s : Sphere P} (hd : s.IsDiameter p₁ p₃) : angle p₁ p₂ p₃ = Real.pi / 2 ↔ p₂ ∈ s

Alias of EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter.

---

Thales' theorem: The angle inscribed in a semicircle is a right angle.

theorem EuclideanGeometry.Sphere.isDiameter_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} {s : Sphere P} [Fact (Module.finrank ℝ V = 2)] (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hne₁₂ : p₁ ≠ p₂) (hne₂₃ : p₂ ≠ p₃) (hangle : angle p₁ p₂ p₃ = Real.pi / 2) : s.IsDiameter p₁ p₃

Converse of Thales' theorem in 2D: if three distinct points on a circle form a right angle, then the chord is a diameter.

theorem EuclideanGeometry.Sphere.IsTangentAt.angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p q : P} {as : AffineSubspace ℝ P} (h : s.IsTangentAt p as) (hq_mem : q ∈ as) : angle q p s.center = Real.pi / 2

For a tangent line to a sphere, the angle between the line and the radius at the tangent point equals π / 2.

theorem EuclideanGeometry.Sphere.IsTangentAt_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p q : P} (h : angle q p s.center = Real.pi / 2) (hp : p ∈ s) : s.IsTangentAt p (affineSpan ℝ {p, q})

If the angle between the line p q and the radius at p equals π / 2, then the line p q is tangent to the sphere at p.

theorem EuclideanGeometry.Sphere.IsTangentAt_iff_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p q : P} (hp : p ∈ s) : s.IsTangentAt p (affineSpan ℝ {p, q}) ↔ angle q p s.center = Real.pi / 2

A line through p is tangent to the sphere at p if and only if the angle between the line and the radius at p equals π / 2.

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

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

theorem EuclideanGeometry.Sphere.two_zsmul_oangle_eq {V : Type u_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : Sphere 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 • oangle p₁ p₂ p₄ = 2 • 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_3} {P : Type u_4} [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} (h : Cospherical {p₁, p₂, p₃, p₄}) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₄ : p₂ ≠ p₄) (hp₃p₁ : p₃ ≠ p₁) (hp₃p₄ : p₃ ≠ p₄) : 2 • oangle p₁ p₂ p₄ = 2 • 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_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) : oangle p₁ s.center p₂ = ↑Real.pi - 2 • 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_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) : oangle p₁ s.center p₂ = ↑Real.pi - 2 • 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_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : Sphere 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 • oangle p₃ p₁ s.center + 2 • 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_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) : |(oangle s.center p₂ p₁).toReal| < 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_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) : |(oangle p₂ p₁ s.center).toReal| < 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_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) : ((oangle p₂ p₁ s.center).tan / 2) • (o.rotation ↑(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_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : Sphere 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₃) : ((oangle p₁ p₂ p₃).tan⁻¹ / 2) • (o.rotation ↑(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_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) : dist p₁ p₂ / (oangle p₂ p₁ s.center).cos / 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_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) : dist p₁ p₂ / (oangle p₂ p₁ s.center).cos = 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_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : Sphere 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₃ / |(oangle p₁ p₂ p₃).sin| / 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_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : Sphere 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₃ / |(oangle p₁ p₂ p₃).sin| = 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 (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : ((EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).tan⁻¹ / 2) • (EuclideanGeometry.o.rotation ↑(Real.pi / 2)) (t.points i₃ -ᵥ t.points i₁) +ᵥ midpoint ℝ (t.points i₁) (t.points i₃) = 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 (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : dist (t.points i₁) (t.points i₃) / |(EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).sin| / 2 = 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 (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : dist (t.points i₁) (t.points i₃) / |(EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).sin| = 2 * 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 (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : Simplex.circumsphere t = { center := ((EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).tan⁻¹ / 2) • (EuclideanGeometry.o.rotation ↑(Real.pi / 2)) (t.points i₃ -ᵥ t.points i₁) +ᵥ midpoint ℝ (t.points i₁) (t.points i₃), radius := dist (t.points i₁) (t.points i₃) / |(EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).sin| / 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 (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {t₁ t₂ : Triangle ℝ P} {i₁ i₂ 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₃)) : Simplex.circumsphere t₁ = 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 (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {t : Triangle ℝ P} {p : P} {i₁ i₂ 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 ∈ 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 Affine.Triangle.dist_div_sin_angle_div_two_eq_circumradius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : dist (t.points i₁) (t.points i₃) / Real.sin (EuclideanGeometry.angle (t.points i₁) (t.points i₂) (t.points i₃)) / 2 = Simplex.circumradius t

The circumradius of a triangle may be expressed explicitly as half the length of a side divided by 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_angle_eq_two_mul_circumradius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : dist (t.points i₁) (t.points i₃) / Real.sin (EuclideanGeometry.angle (t.points i₁) (t.points i₂) (t.points i₃)) = 2 * Simplex.circumradius t

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

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 (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ : P} (h : 2 • oangle p₁ p₂ p₄ = 2 • oangle p₁ p₃ p₄) (hn : ¬Collinear ℝ {p₁, p₂, p₄}) : 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 (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ : P} (h : 2 • oangle p₁ p₂ p₄ = 2 • oangle p₁ p₃ p₄) (hn : ¬Collinear ℝ {p₁, p₂, p₄}) : 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 (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ : P} (h : 2 • oangle p₁ p₂ p₄ = 2 • oangle p₁ p₃ p₄) : 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 (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ : P} (h : 2 • oangle p₁ p₂ p₄ = 2 • oangle p₁ p₃ p₄) : 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.