# mathlib3documentation

geometry.euclidean.angle.sphere

# Angles in circles and sphere. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [fact (fdim V = 2)] (o : (fin 2)) {x y z : V} (hxyne : x y) (hxzne : x z) (hxy : x = y) (hxz : x = z) :
o.oangle y z = 2 o.oangle (y - x) (z - x)

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

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

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

theorem orientation.two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq {V : Type u_1} [fact (fdim V = 2)] (o : (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 euclidean_geometry.sphere.oangle_center_eq_two_zsmul_oangle {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (hp₁ : p₁ s) (hp₂ : p₂ s) (hp₃ : p₃ s) (hp₂p₁ : p₂ p₁) (hp₂p₃ : p₂ p₃) :
p₃ = 2 p₃

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

theorem euclidean_geometry.sphere.two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {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 p₄ = 2 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 euclidean_geometry.cospherical.two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ p₄ : P} (h : euclidean_geometry.cospherical {p₁, p₂, p₃, p₄}) (hp₂p₁ : p₂ p₁) (hp₂p₄ : p₂ p₄) (hp₃p₁ : p₃ p₁) (hp₃p₄ : p₃ p₄) :
2 p₄ = 2 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 euclidean_geometry.sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_left {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ : P} (hp₁ : p₁ s) (hp₂ : p₂ s) (h : p₁ p₂) :
p₂ = real.pi - 2 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 euclidean_geometry.sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_right {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ : P} (hp₁ : p₁ s) (hp₂ : p₂ s) (h : p₁ p₂) :
p₂ = real.pi - 2 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 euclidean_geometry.sphere.two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {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 s.center + 2 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 euclidean_geometry.sphere.abs_oangle_center_left_to_real_lt_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ : P} (hp₁ : p₁ s) (hp₂ : p₂ s) :
| p₁).to_real| <

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

theorem euclidean_geometry.sphere.abs_oangle_center_right_to_real_lt_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ : P} (hp₁ : p₁ s) (hp₂ : p₂ s) :

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

theorem euclidean_geometry.sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ : P} (hp₁ : p₁ s) (hp₂ : p₂ s) (h : p₁ p₂) :
p₁ s.center).tan / 2) (p₂ -ᵥ p₁) +ᵥ 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 euclidean_geometry.sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {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₃) :
p₂ p₃).tan)⁻¹ / 2) (p₃ -ᵥ p₁) +ᵥ 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 euclidean_geometry.sphere.dist_div_cos_oangle_center_div_two_eq_radius {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ : P} (hp₁ : p₁ s) (hp₂ : p₂ s) (h : p₁ 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 euclidean_geometry.sphere.dist_div_cos_oangle_center_eq_two_mul_radius {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ : P} (hp₁ : p₁ s) (hp₂ : p₂ s) (h : p₁ 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 euclidean_geometry.sphere.dist_div_sin_oangle_div_two_eq_radius {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {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₃) :
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 euclidean_geometry.sphere.dist_div_sin_oangle_eq_two_mul_radius {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {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₃) :
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} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] (t : P) {i₁ i₂ i₃ : fin 3} (h₁₂ : i₁ i₂) (h₁₃ : i₁ i₃) (h₂₃ : i₂ i₃) :
(((euclidean_geometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).tan)⁻¹ / 2) (t.points i₃ -ᵥ t.points i₁) +ᵥ (t.points i₁) (t.points i₃) =

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} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] (t : P) {i₁ i₂ i₃ : fin 3} (h₁₂ : i₁ i₂) (h₁₃ : i₁ i₃) (h₂₃ : i₂ i₃) :
has_dist.dist (t.points i₁) (t.points i₃) / |(euclidean_geometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).sin| / 2 =

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} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] (t : P) {i₁ i₂ i₃ : fin 3} (h₁₂ : i₁ i₂) (h₁₃ : i₁ i₃) (h₂₃ : i₂ i₃) :
has_dist.dist (t.points i₁) (t.points i₃) / |(euclidean_geometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).sin| =

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} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] (t : P) {i₁ i₂ i₃ : fin 3} (h₁₂ : i₁ i₂) (h₁₃ : i₁ i₃) (h₂₃ : i₂ i₃) :
= {center := (((euclidean_geometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).tan)⁻¹ / 2) (t.points i₃ -ᵥ t.points i₁) +ᵥ (t.points i₁) (t.points i₃), radius := has_dist.dist (t.points i₁) (t.points i₃) / |(euclidean_geometry.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} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {t₁ t₂ : 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 euclidean_geometry.oangle (t₁.points i₁) (t₁.points i₂) (t₁.points i₃) = 2 euclidean_geometry.oangle (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)) :

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} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {t : P} {p : P} {i₁ i₂ i₃ : fin 3} (h₁₂ : i₁ i₂) (h₁₃ : i₁ i₃) (h₂₃ : i₂ i₃) (h : 2 p (t.points i₃) = 2 (t.points i₂) (t.points i₃)) :

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 euclidean_geometry.cospherical_of_two_zsmul_oangle_eq_of_not_collinear {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ p₄ : P} (h : 2 p₄ = 2 p₄) (hn : ¬ {p₁, p₂, p₄}) :
euclidean_geometry.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 euclidean_geometry.concyclic_of_two_zsmul_oangle_eq_of_not_collinear {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ p₄ : P} (h : 2 p₄ = 2 p₄) (hn : ¬ {p₁, p₂, p₄}) :
euclidean_geometry.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 euclidean_geometry.cospherical_or_collinear_of_two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ p₄ : P} (h : 2 p₄ = 2 p₄) :
euclidean_geometry.cospherical {p₁, p₂, p₃, p₄} {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 euclidean_geometry.concyclic_or_collinear_of_two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ p₄ : P} (h : 2 p₄ = 2 p₄) :
euclidean_geometry.concyclic {p₁, p₂, p₃, p₄} {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.