geometry.euclidean.angle.sphere

source

theorem orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim 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)

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

source

theorem orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim 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)

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

source

theorem orientation.two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [fact (fdim 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.

source

theorem euclidean_geometry.sphere.oangle_center_eq_two_zsmul_oangle {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {s : euclidean_geometry.sphere P} {p₁ p₂ p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₃ : p₂ ≠ p₃) :

euclidean_geometry.oangle p₁ s.center p₃ = 2 • euclidean_geometry.oangle p₁ p₂ p₃

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

source

theorem euclidean_geometry.sphere.two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {s : euclidean_geometry.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 • euclidean_geometry.oangle p₁ p₂ p₄ = 2 • euclidean_geometry.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.

source

theorem euclidean_geometry.cospherical.two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (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 • euclidean_geometry.oangle p₁ p₂ p₄ = 2 • euclidean_geometry.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.

source

theorem euclidean_geometry.sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_left {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {s : euclidean_geometry.sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) :

euclidean_geometry.oangle p₁ s.center p₂ = ↑real.pi - 2 • euclidean_geometry.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.

source

theorem euclidean_geometry.sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_right {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {s : euclidean_geometry.sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) :

euclidean_geometry.oangle p₁ s.center p₂ = ↑real.pi - 2 • euclidean_geometry.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.

source

theorem euclidean_geometry.sphere.two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {s : euclidean_geometry.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 • euclidean_geometry.oangle p₃ p₁ s.center + 2 • euclidean_geometry.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 π.

source

theorem euclidean_geometry.sphere.abs_oangle_center_left_to_real_lt_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {s : euclidean_geometry.sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) :

|(euclidean_geometry.oangle s.center p₂ p₁).to_real| < real.pi / 2

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

source

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

|(euclidean_geometry.oangle p₂ p₁ s.center).to_real| < real.pi / 2

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

source

theorem euclidean_geometry.sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {s : euclidean_geometry.sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) :

((euclidean_geometry.oangle p₂ p₁ s.center).tan / 2) • ⇑(module.oriented.positive_orientation.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.

source

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} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {s : euclidean_geometry.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₃) :

(((euclidean_geometry.oangle p₁ p₂ p₃).tan)⁻¹ / 2) • ⇑(module.oriented.positive_orientation.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.

source

theorem euclidean_geometry.sphere.dist_div_cos_oangle_center_div_two_eq_radius {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {s : euclidean_geometry.sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) :

has_dist.dist p₁ p₂ / (euclidean_geometry.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.

source

theorem euclidean_geometry.sphere.dist_div_cos_oangle_center_eq_two_mul_radius {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {s : euclidean_geometry.sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) :

has_dist.dist p₁ p₂ / (euclidean_geometry.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.

source

theorem euclidean_geometry.sphere.dist_div_sin_oangle_div_two_eq_radius {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {s : euclidean_geometry.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₃) :

has_dist.dist p₁ p₃ / |(euclidean_geometry.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).

source

theorem euclidean_geometry.sphere.dist_div_sin_oangle_eq_two_mul_radius {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {s : euclidean_geometry.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₃) :

has_dist.dist p₁ p₃ / |(euclidean_geometry.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).

source

theorem affine.triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] (t : affine.triangle ℝ 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) • ⇑(module.oriented.positive_orientation.rotation ↑(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.

source

theorem affine.triangle.dist_div_sin_oangle_div_two_eq_circumradius {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] (t : affine.triangle ℝ 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 = 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).

source

theorem affine.triangle.dist_div_sin_oangle_eq_two_mul_circumradius {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] (t : affine.triangle ℝ 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 * 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).

source

theorem affine.triangle.circumsphere_eq_of_dist_of_oangle {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] (t : affine.triangle ℝ P) {i₁ i₂ i₃ : fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) :

affine.simplex.circumsphere t = {center := (((euclidean_geometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).tan)⁻¹ / 2) • ⇑(module.oriented.positive_orientation.rotation ↑(real.pi / 2)) (t.points i₃ -ᵥ t.points i₁) +ᵥ midpoint ℝ (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.

source

theorem affine.triangle.circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {t₁ t₂ : affine.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 • 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₃)) :

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.

source

theorem affine.triangle.mem_circumsphere_of_two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {t : affine.triangle ℝ P} {p : P} {i₁ i₂ i₃ : fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) (h : 2 • euclidean_geometry.oangle (t.points i₁) p (t.points i₃) = 2 • euclidean_geometry.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.

source

theorem euclidean_geometry.cospherical_of_two_zsmul_oangle_eq_of_not_collinear {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ p₄ : P} (h : 2 • euclidean_geometry.oangle p₁ p₂ p₄ = 2 • euclidean_geometry.oangle p₁ p₃ p₄) (hn : ¬collinear ℝ {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 π.

source

theorem euclidean_geometry.concyclic_of_two_zsmul_oangle_eq_of_not_collinear {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ p₄ : P} (h : 2 • euclidean_geometry.oangle p₁ p₂ p₄ = 2 • euclidean_geometry.oangle p₁ p₃ p₄) (hn : ¬collinear ℝ {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.

source

theorem euclidean_geometry.cospherical_or_collinear_of_two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ p₄ : P} (h : 2 • euclidean_geometry.oangle p₁ p₂ p₄ = 2 • euclidean_geometry.oangle p₁ p₃ p₄) :

euclidean_geometry.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.

source

theorem euclidean_geometry.concyclic_or_collinear_of_two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ p₄ : P} (h : 2 • euclidean_geometry.oangle p₁ p₂ p₄ = 2 • euclidean_geometry.oangle p₁ p₃ p₄) :

euclidean_geometry.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.

mathlib3 documentation

Angles in circles and sphere. #