EuclideanGeometry.Sphere.dist_div_sin_oangle_eq_two_mul_radius
theorem EuclideanGeometry.Sphere.dist_div_sin_oangle_eq_two_mul_radius :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P},
p₁ ∈ s →
p₂ ∈ s →
p₃ ∈ s →
p₁ ≠ p₂ → p₁ ≠ p₃ → p₂ ≠ p₃ → dist p₁ p₃ / |(EuclideanGeometry.oangle p₁ p₂ p₃).sin| = 2 * s.radius
This theorem, deriving from Euclidean Geometry and Trigonometry on a sphere, states that given any three distinct points `p₁`, `p₂`, and `p₃` on a circle (or sphere `s`), the ratio of the distance between `p₁` and `p₃` to the absolute value of the sine of the angle at `p₂` is equal to twice the radius of the sphere. This theorem is a variant of the law of sines, also known as the sine rule. The space in which the points and the sphere exist is a 2-dimensional vector space over the field of real numbers, equipped with a Euclidean metric and an orientation.
More concisely: Given three distinct points on a sphere, the ratio of the distance between any two of them to the sine of the angle between them is twice the sphere's radius.
|
EuclideanGeometry.Sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center
theorem EuclideanGeometry.Sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
p₁ ∈ s →
p₂ ∈ s →
p₁ ≠ p₂ →
((EuclideanGeometry.oangle p₂ p₁ s.center).tan / 2) •
(EuclideanGeometry.o.rotation ↑(Real.pi / 2)) (p₂ -ᵥ p₁) +ᵥ
midpoint ℝ p₁ p₂ =
s.center
This theorem states that, given two distinct points on a circle, the center of that circle can be computed using the vector from the first point to the second, the midpoint of the two points, and the tangent of half the angle between the chord and the radius at one of the points. Specifically, it can be expressed as a sum of the midpoint and the vector from the first point to the second, rotated by 90 degrees (π / 2 radians), then scaled by half the tangent of the angle between the chord from the first point to the second and the radius at the first point. This theorem applies in a two-dimensional Euclidean space, as specified by the condition that the finite rank of the vector space is 2.
More concisely: Given two distinct points on a circle in 2-dimensional Euclidean space, the circle's center is the midpoint between the points plus half the length of the vector between them, rotated 90 degrees counterclockwise and scaled by the tangent of half the angle between the chord and the radius at one of the points.
|
EuclideanGeometry.concyclic_of_two_zsmul_oangle_eq_of_not_collinear
theorem EuclideanGeometry.concyclic_of_two_zsmul_oangle_eq_of_not_collinear :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ : P},
2 • EuclideanGeometry.oangle p₁ p₂ p₄ = 2 • EuclideanGeometry.oangle p₁ p₃ p₄ →
¬Collinear ℝ {p₁, p₂, p₄} → EuclideanGeometry.Concyclic {p₁, p₂, p₃, p₄}
This theorem, named `EuclideanGeometry.concyclic_of_two_zsmul_oangle_eq_of_not_collinear`, states the following: Given a normed add commutative group `V` and an inner product space over `V` with the real numbers, a metric space `P` and a normed add torsor over `P` with `V`, and an oriented module over `V` with dimension 2, for any four points `p₁`, `p₂`, `p₃`, and `p₄` in `P`, if twice the oriented angle between `p₁`, `p₂`, and `p₄` is equal to twice the oriented angle between `p₁`, `p₃`, and `p₄`, and if `p₁`, `p₂`, and `p₄` are not collinear (i.e., they do not lie on the same straight line), then the four points `p₁`, `p₂`, `p₃`, and `p₄` are concyclic (i.e., they lie on the same circle). This is essentially a converse of the classical geometric facts that angles in the same segment of a circle are equal, and that opposite angles of a cyclic quadrilateral sum to 180 degrees, but formulated in the language of oriented angles modulo π.
More concisely: Given an oriented 2-dimensional module over a normed add commutative group with an inner product space and real numbers, if four non-collinear points have equal oriented angles between two pairs, then they are concyclic.
|
Affine.Triangle.dist_div_sin_oangle_div_two_eq_circumradius
theorem Affine.Triangle.dist_div_sin_oangle_div_two_eq_circumradius :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
i₁ ≠ i₂ →
i₁ ≠ i₃ →
i₂ ≠ i₃ →
dist (t.points i₁) (t.points i₃) /
|(EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).sin| /
2 =
Affine.Simplex.circumradius t
This theorem states that for a triangle in a 2-dimensional real vector space, the circumradius of the triangle can be explicitly expressed as half the length of one of its sides divided by the absolute value of the sine of the angle at the opposing vertex. This is a variant of the law of sines, also known as the sine rule. Specifically, given three non-equal indices `i₁`, `i₂`, and `i₃` representing the vertices of the triangle, the distance between the points at `i₁` and `i₃`, divided by the absolute value of the sine of the angle formed by the points at `i₁`, `i₂`, and `i₃`, and then further divided by 2, equals the circumradius of the triangle.
More concisely: The circumradius of a triangle in a 2-dimensional real vector space is given by half the length of one of its sides divided by the sine of the angle at the opposing vertex. (This is a variant of the law of sines, also known as the sine rule.)
|
EuclideanGeometry.concyclic_or_collinear_of_two_zsmul_oangle_eq
theorem EuclideanGeometry.concyclic_or_collinear_of_two_zsmul_oangle_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ : P},
2 • EuclideanGeometry.oangle p₁ p₂ p₄ = 2 • EuclideanGeometry.oangle p₁ p₃ p₄ →
EuclideanGeometry.Concyclic {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}
This theorem, titled `concyclic_or_collinear_of_two_zsmul_oangle_eq`, states that for any four points `p₁, p₂, p₃, p₄` in a 2-dimensional Euclidean Space with a fixed orientation, if the double of the oriented angle from `p₁` through `p₂` to `p₄` equals the double of the oriented angle from `p₁` through `p₃` to `p₄`, then the four points are either concyclic (they lie on the same circle) or collinear (they lie on the same straight line). This is essentially the reverse of two theorems from Euclidean geometry: that angles in the same segment of a circle are equal, and that opposite angles of a cyclic quadrilateral sum to π, but considered in the context of oriented angles modulo π.
More concisely: Given any four points `p₁, p₂, p₃, p₄` in a 2-dimensional Euclidean Space with a fixed orientation, if the double of the oriented angle from `p₁` through `p₂` to `p₄` equals the double of the oriented angle from `p₁` through `p₃` to `p₄`, then the four points are either collinear or concyclic.
|
Orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real
theorem Orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y z : V},
x ≠ y → x ≠ z → ∀ {r : ℝ}, ‖x‖ = r → ‖y‖ = r → ‖z‖ = r → o.oangle y z = 2 • o.oangle (y - x) (z - x)
The theorem `Orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real` asserts that in a 2-dimensional real inner product space, given an orientation and three vectors x, y, and z, all of which have the same norm r and are distinct from each other, the oriented angle between vectors y and z is twice the oriented angle between vectors (y - x) and (z - x). This theorem is a generalization of the geometric principle that the angle subtended by a chord at the center of a circle is twice the angle subtended by the same chord at the circumference.
More concisely: In a 2-dimensional real inner product space, for vectors x, y, and z of equal norm and distinct from each other, the oriented angle between y and z is twice the oriented angle between (y - x) and (z - x).
|
EuclideanGeometry.Cospherical.two_zsmul_oangle_eq
theorem EuclideanGeometry.Cospherical.two_zsmul_oangle_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ : P},
EuclideanGeometry.Cospherical {p₁, p₂, p₃, p₄} →
p₂ ≠ p₁ →
p₂ ≠ p₄ → p₃ ≠ p₁ → p₃ ≠ p₄ → 2 • EuclideanGeometry.oangle p₁ p₂ p₄ = 2 • EuclideanGeometry.oangle p₁ p₃ p₄
This theorem, named `EuclideanGeometry.Cospherical.two_zsmul_oangle_eq`, states the following in plain language:
Given a set of four distinct points `{p₁, p₂, p₃, p₄}` in a two-dimensional inner product space `P` over the real numbers, where the space `P` is equipped with a metric and an orientation, if the points are cospherical - meaning they are all equidistant from some common point - then the oriented angle (`EuclideanGeometry.oangle`) between `p₁ p₂ p₄`, multiplied by two, is equal to the oriented angle between `p₁ p₃ p₄`, also multiplied by two.
In geometric terms, this is a version of the two well-known theorems: "angles in the same segment are equal" and "opposite angles of a cyclic quadrilateral add up to π". However, here the angles are oriented and are considered modulo π, hence the factor of two in the angle equality.
More concisely: In a two-dimensional real inner product space with metric and orientation, the sum of the oriented angles between three distinct points, each pair being cospherical, is equal to 2π.
|
Affine.Triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter
theorem Affine.Triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
i₁ ≠ i₂ →
i₁ ≠ i₃ →
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₃) =
Affine.Simplex.circumcenter t
This theorem states that in a 2-dimensional real Euclidean space, for any triangle with vertices not all the same, the circumcenter of the triangle can be computed as follows: first, calculate the angle at one of the vertices (i.e., the angle formed by that vertex and the other two vertices), take its tangent, and then the reciprocal of this value. Divide this by 2 and use this as a scalar to rotate the vector between the other two vertices by $\frac{\pi}{2}$ (90 degrees). Finally, add to this rotated vector the midpoint of the line segment between the two other vertices. The resultant point is the circumcenter of the triangle.
More concisely: In a 2-dimensional real Euclidean space, the circumcenter of a triangle with vertices at A, B, and C is the point given by the vector obtained by rotating the vector AB by 90 degrees around the origin, then scaling by the reciprocal of the tangent of the angle at vertex A, and adding the midpoint of BC.
|
Orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq
theorem Orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y z : V},
x ≠ y → x ≠ z → ‖x‖ = ‖y‖ → ‖x‖ = ‖z‖ → o.oangle y z = 2 • o.oangle (y - x) (z - x)
The theorem `Orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq` states that for any vector space `V` which is a normed add commutative group and an inner product space over the real numbers, and has finite dimension equal to 2, along with given orientation `o` (Orientation is a concept in mathematics that in particular case is used to specify the rotational direction of basis vectors), if we consider any three vectors `x`, `y`, and `z` in that vector space such that `x` is not equal to `y` and `x` is not equal to `z`, and also the norm (or "length") of the vector `x` is equal to the norms of vectors `y` and `z`, then the oriented angle between vectors `y` and `z` is equal to twice the oriented angle between vectors `y - x` and `z - x`. This theorem is a generalized form of the geometric fact that the angle at the center of a circle is twice the angle at the circumference when subtended by the same arc.
More concisely: For any 2-dimensional normed add commutative group and inner product space over the real numbers with given orientation, if the norms of vectors $y-x$ and $z-x$ are equal, then the oriented angle between $y$ and $z$ is twice the oriented angle between $y-x$ and $z-x$.
|
EuclideanGeometry.Sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center
theorem EuclideanGeometry.Sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P},
p₁ ∈ s →
p₂ ∈ s →
p₃ ∈ s →
p₁ ≠ p₂ →
p₁ ≠ p₃ →
p₂ ≠ p₃ →
((EuclideanGeometry.oangle p₁ p₂ p₃).tan⁻¹ / 2) •
(EuclideanGeometry.o.rotation ↑(Real.pi / 2)) (p₃ -ᵥ p₁) +ᵥ
midpoint ℝ p₁ p₃ =
s.center
This theorem states that given three distinct points on a sphere in a 2-dimensional real inner product space, the center of that sphere can be calculated as follows: multiply half the inverse of the tangent of the oriented angle at one of the points by the result of rotating the vector from the first to the third point by π/2 radians, and then add this to the midpoint of the first and third points. The oriented angle is computed according to a fixed positive orientation of the space.
More concisely: Given three distinct points on the surface of a 2-dimensional real sphere, the sphere's center is the midpoint between the first two points plus half the normal vector of the plane containing the first and third points rotated counter-clockwise by π/2 radians.
|
EuclideanGeometry.Sphere.abs_oangle_center_right_toReal_lt_pi_div_two
theorem EuclideanGeometry.Sphere.abs_oangle_center_right_toReal_lt_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
p₁ ∈ s → p₂ ∈ s → |(EuclideanGeometry.oangle p₂ p₁ s.center).toReal| < Real.pi / 2
This theorem states that in any given 2-dimensional Euclidean space (as guaranteed by the assumption `FiniteDimensional.finrank ℝ V = 2`), for any sphere defined within that space, if you pick two points on the sphere (`p₁` and `p₂`), the absolute value of the oriented angle between the line from `p₂` to the center of the sphere and the line from `p₁` to the center is less than π/2. In other words, the base angle of an isosceles triangle formed by two points on the sphere and the center of the sphere (with the apex at the center) is acute. This is a generalization of the geometric fact that in an isosceles triangle, the base angles are always acute.
More concisely: In a 2-dimensional Euclidean space, for any sphere and any two points on it, the oriented angle between the radii from these points to the sphere's center is less than π/2.
|
Orientation.two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq
theorem Orientation.two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x₁ x₂ y z : V},
x₁ ≠ y →
x₁ ≠ z →
x₂ ≠ y →
x₂ ≠ z →
∀ {r : ℝ},
‖x₁‖ = r →
‖x₂‖ = r → ‖y‖ = r → ‖z‖ = r → 2 • o.oangle (y - x₁) (z - x₁) = 2 • o.oangle (y - x₂) (z - x₂)
This theorem, named "Orientation.two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq", states an oriented vector version of the geometric principles that "angles in the same segment are equal" and "opposite angles of a cyclic quadrilateral add up to π". Specifically, it addresses the case of oriented angles mod π, for which these two geometric principles are equivalent. The theorem asserts that for any 2-dimensional vector space `V` over real numbers `ℝ` with a given orientation `o`, if `x₁`, `x₂`, `y`, `z` are distinct vectors in `V` all with the same norm `r`, then the double of the oriented angle between `y - x₁` and `z - x₁` is equal to the double of the oriented angle between `y - x₂` and `z - x₂`.
More concisely: For any 2-dimensional real vector space with a given orientation, the double of the oriented angle between `y - x₁` and `z - x₁`, and `y - x₂` and `z - x₂`, are equal, given that `x₁`, `x₂`, `y`, `z` are distinct vectors with the same norm.
|
EuclideanGeometry.Sphere.two_zsmul_oangle_eq
theorem EuclideanGeometry.Sphere.two_zsmul_oangle_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ p₄ : P},
p₁ ∈ s →
p₂ ∈ s →
p₃ ∈ s →
p₄ ∈ s →
p₂ ≠ p₁ →
p₂ ≠ p₄ →
p₃ ≠ p₁ → p₃ ≠ p₄ → 2 • EuclideanGeometry.oangle p₁ p₂ p₄ = 2 • EuclideanGeometry.oangle p₁ p₃ p₄
This theorem, named `EuclideanGeometry.Sphere.two_zsmul_oangle_eq`, states that in a two-dimensional real inner product space, for any four points `p₁`, `p₂`, `p₃`, `p₄` belonging to the same sphere `s`, provided that `p₂` is different from `p₁` and `p₄`, and `p₃` is different from `p₁` and `p₄`, the oriented angle from `p₁` through `p₂` to `p₄` is the same as the oriented angle from `p₁` through `p₃` to `p₄`, when both angles are scaled by a factor of 2. This is a version of the classic Euclidean geometry results that "angles in the same segment are equal" and "opposite angles of a cyclic quadrilateral add up to π", but it is formulated for oriented angles modulo π, and the equality is about twice the original angles.
More concisely: In a 2-dimensional real inner product space, for any four distinct points on the same sphere, the twice-signed oriented angle from the first point to the third, is equal to the twice-signed oriented angle from the first point to the fourth.
|
Affine.Triangle.mem_circumsphere_of_two_zsmul_oangle_eq
theorem Affine.Triangle.mem_circumsphere_of_two_zsmul_oangle_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {t : Affine.Triangle ℝ P} {p : P} {i₁ i₂ i₃ : Fin 3},
i₁ ≠ i₂ →
i₁ ≠ i₃ →
i₂ ≠ i₃ →
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
This theorem is stating that given a triangle, and another point such that the double of the angle between two points of the triangle at this additional point equals the double of the third angle of the triangle, then this additional point lies on the circumsphere of the triangle.
In more detail, it says that for a normed add commutative group `V`, an inner product space over `ℝ` on `V`, a metric space `P`, a normed add torsor over `P`, a fact that the finite rank of `V` over `ℝ` is 2, an oriented module over `ℝ` and `V` with 2 elements, a triangle `t` and a point `p`, if any three points in the triangle are different (not equal), and the double of the angle between the first and third points of the triangle at point `p` equals the double of the angle between the first, the second and the third points of the triangle, then point `p` belongs to the circumsphere of the triangle `t`.
More concisely: Given a triangle in a Euclidean plane with an additional point such that the angle between any two triangle sides at this point equals twice the corresponding interior angle of the triangle, then this point lies on the triangle's circumsphere.
|
Affine.Triangle.circumsphere_eq_of_dist_of_oangle
theorem Affine.Triangle.circumsphere_eq_of_dist_of_oangle :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
i₁ ≠ i₂ →
i₁ ≠ i₃ →
i₂ ≠ i₃ →
Affine.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 }
This theorem states that for any triangle (in a normed additively commutative group `V` that is an inner product space over the reals, equipped with a metric space structure `P` and torsors `V P`, and whose real rank is 2 and is oriented) represented by `t`, and any three distinct indices `i₁, i₂, i₃` (referring to the vertices of the triangle), the circumsphere (the sphere that passes through all the vertices) of the triangle can be explicitly computed. Specifically, the center of the circumsphere is given by the midpoint of the vector formed by `t.points i₁` and `t.points i₃`, rotated by the angle `π/2` and scaled by the tangent of half of the oriented angle formed by `t.points i₁, t.points i₂, t.points i₃`. The radius of the circumsphere is the distance between `t.points i₁` and `t.points i₃`, divided by twice of the absolute value of the sine of the oriented angle formed by `t.points i₁, t.points i₂, t.points i₃`.
More concisely: Given a triangle in a 2-dimensional real inner product space `V` with metric `P`, the center of its circumsphere is the midpoint between two vertices rotated by π/2 and scaled by the tangent of half the oriented angle between them, and the radius is half the distance between the third vertex and the midpoint multiplied by the sine of half the oriented angle.
|
EuclideanGeometry.Sphere.dist_div_cos_oangle_center_div_two_eq_radius
theorem EuclideanGeometry.Sphere.dist_div_cos_oangle_center_div_two_eq_radius :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
p₁ ∈ s → p₂ ∈ s → p₁ ≠ p₂ → dist p₁ p₂ / (EuclideanGeometry.oangle p₂ p₁ s.center).cos / 2 = s.radius
This theorem states that for any two different points on a circle in a two-dimensional Euclidean space, the radius of the circle can be expressed as half of the distance between these two points divided by the cosine of the angle between the line segment joining the two points (or chord) and the radius at one of the points. This theorem applies in the context of a normed add commutative group, an inner product space over the real numbers, a metric space, a normed add torsor, and an oriented module.
More concisely: The radius of a circle in a Euclidean space is given by the distance between two distinct points on the circle divided by twice the cosine of half the angle between the chord connecting them and a radius at one point.
|
EuclideanGeometry.Sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_right
theorem EuclideanGeometry.Sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_right :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
p₁ ∈ s →
p₂ ∈ s →
p₁ ≠ p₂ → EuclideanGeometry.oangle p₁ s.center p₂ = ↑Real.pi - 2 • EuclideanGeometry.oangle p₂ p₁ s.center
This theorem establishes a key property of an isosceles triangle in Euclidean geometry. It states that for any two distinct points `p₁` and `p₂` on a sphere `s` in a 2-dimensional vector space `V` over the real numbers, the oriented angle at the sphere's center point (considered as the apex of an isosceles triangle) between `p₁` and `p₂` is equal to the mathematical constant π (`Real.pi` in Lean 4, approximately 3.14159265) minus twice the oriented angle at `p₂` between `p₁` and the sphere's center. This property holds when `V` is a normed add commutative group, an inner product space, and a module oriented over the reals, and `P` is a metric space where `V` acts freely and transitively.
More concisely: In a 2-dimensional normed, inner product space over the real numbers, the angle at the sphere's center between two distinct points on the sphere is equal to PI minus twice the angle at one point between them.
|
EuclideanGeometry.Sphere.dist_div_cos_oangle_center_eq_two_mul_radius
theorem EuclideanGeometry.Sphere.dist_div_cos_oangle_center_eq_two_mul_radius :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
p₁ ∈ s → p₂ ∈ s → p₁ ≠ p₂ → dist p₁ p₂ / (EuclideanGeometry.oangle p₂ p₁ s.center).cos = 2 * s.radius
This theorem, in the context of Euclidean Geometry, states that for any two distinct points on a sphere, the division of the distance between these two points by the cosine of the angle formed between the line segment joining the two points (chord) and the radius at one point, gives twice the radius of the sphere. This holds true in a 2-dimensional vector space over the real numbers ℝ. The sphere, points, and vector space involved all adhere to certain algebraic structures such as being a metric space, a normed add torsor, and an inner product space, respectively.
More concisely: In Euclidean geometry, the quotient of the distance between two distinct points on a sphere and the cosine of the angle between the line segment joining them and the radius at one point is twice the radius of the sphere.
|
Affine.Triangle.dist_div_sin_oangle_eq_two_mul_circumradius
theorem Affine.Triangle.dist_div_sin_oangle_eq_two_mul_circumradius :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
i₁ ≠ i₂ →
i₁ ≠ i₃ →
i₂ ≠ i₃ →
dist (t.points i₁) (t.points i₃) /
|(EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).sin| =
2 * Affine.Simplex.circumradius t
This theorem provides an explicit expression for twice the circumradius of a triangle in terms of side lengths and angles. Specifically, in a normed affine space over the real numbers with a two-dimensional, oriented real vector module, for any triangle and its three non-identical vertices, the distance between two vertices divided by the absolute value of the sine of the angle at the third vertex equals two times the circumradius of the triangle. This theorem is a variant of the law of sines, also known as the sine rule.
More concisely: In a triangle with side lengths $a, b, c$ and angles $\alpha, \beta, \gamma$, the circumradius $R$ satisfies $R \cdot (\sin \alpha) = \frac{1}{2} \cdot (\frac{a}{2} \cdot \sin \beta + \frac{b}{2} \cdot \sin \gamma)$.
|
Affine.Triangle.circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq
theorem Affine.Triangle.circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {t₁ t₂ : Affine.Triangle ℝ P} {i₁ i₂ i₃ : Fin 3},
i₁ ≠ i₂ →
i₁ ≠ i₃ →
i₂ ≠ i₃ →
t₁.points i₁ = t₂.points i₁ →
t₁.points i₃ = t₂.points i₃ →
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₂
The theorem states that, given two triangles in a two-dimensional vector space over the real numbers, if the triangles share two points and the double of the angle at the third point in each triangle is the same, then they share the same circumsphere. The circumsphere of a triangle is a sphere that passes through all the vertices of the triangle. This theorem requires that the points defining the triangles are distinct and that the vector space has an orientation.
More concisely: Given two distinct triangles in a 2-dimensional real vector space with an orientation, if two angles at corresponding vertices differ by a constant and the third angles are supplementary, then their circumspheres are congruent.
|
EuclideanGeometry.Sphere.dist_div_sin_oangle_div_two_eq_radius
theorem EuclideanGeometry.Sphere.dist_div_sin_oangle_div_two_eq_radius :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P},
p₁ ∈ s →
p₂ ∈ s →
p₃ ∈ s →
p₁ ≠ p₂ → p₁ ≠ p₃ → p₂ ≠ p₃ → dist p₁ p₃ / |(EuclideanGeometry.oangle p₁ p₂ p₃).sin| / 2 = s.radius
This theorem, from Euclidean Geometry, states that given any three distinct points `p₁`, `p₂`, and `p₃` on a sphere `s` in a two-dimensional real inner product space, the radius of the sphere can be computed from these points as follows. The radius is half the distance from `p₁` to `p₃` divided by the absolute value of the sine of the oriented angle at `p₂` formed by `p₁`, `p₂`, and `p₃`. This is a variant of the law of sines. The theorem demands that the considered vector space has an orientation and is two-dimensional.
More concisely: The radius of a sphere in a 2-dimensional real inner product space with points `p₁`, `p₂`, and `p₃` on its surface is given by the formula: radius = 0.5 * ||p₁ - p₃|| / |sin(angle between p₁p₂ and p₁p₃)|, where ||.|| denotes the Euclidean norm and angle is the oriented angle between the vectors p₁p₂ and p₁p₃.
|
EuclideanGeometry.cospherical_of_two_zsmul_oangle_eq_of_not_collinear
theorem EuclideanGeometry.cospherical_of_two_zsmul_oangle_eq_of_not_collinear :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ : P},
2 • EuclideanGeometry.oangle p₁ p₂ p₄ = 2 • EuclideanGeometry.oangle p₁ p₃ p₄ →
¬Collinear ℝ {p₁, p₂, p₄} → EuclideanGeometry.Cospherical {p₁, p₂, p₃, p₄}
This theorem states that given a vector space `V` over the reals with an inner product and normed add torsor `P`, and under the assumption that the dimension of `V` is `2`, if the oriented angles `p₁, p₂, p₄` and `p₁, p₃, p₄` are equal (where the angle is multiplied by 2), and the points `p₁`, `p₂`, and `p₄` are not collinear, then the points `p₁`, `p₂`, `p₃`, and `p₄` are cospherical. In simpler terms, this theorem provides a condition under which a set of four points in a 2-dimensional vector space are all equidistant from some common point (cospherical), given that two pairs of them form equal angles and they are not all on a single line.
More concisely: In a 2-dimensional real vector space with an inner product and normed additive torsor, if two pairs of non-collinear points form equal angles and their oriented differences are in the torsor, then the points are cospherical.
|
EuclideanGeometry.Sphere.abs_oangle_center_left_toReal_lt_pi_div_two
theorem EuclideanGeometry.Sphere.abs_oangle_center_left_toReal_lt_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
p₁ ∈ s → p₂ ∈ s → |(EuclideanGeometry.oangle s.center p₂ p₁).toReal| < Real.pi / 2
This theorem states that in a Euclidean geometry setting, the base angle of an isosceles triangle, where the apex is at the center of a sphere, is always less than $\pi/2$. More formally, for a sphere `s` in a real inner product space of finite dimension 2, with any two points `p₁` and `p₂` on the sphere, the absolute value of the angle (measured in radians) between the center of the sphere to `p₂` and the center to `p₁` is less than $\pi/2$. The angle is considered positive if it is oriented counterclockwise, and negative otherwise.
More concisely: In a Euclidean geometry setting, the angle between any two points on a sphere's surface and the sphere's center is less than $\pi/2$ in magnitude.
|
EuclideanGeometry.Sphere.two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi
theorem EuclideanGeometry.Sphere.two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P},
p₁ ∈ s →
p₂ ∈ s →
p₃ ∈ s →
p₂ ≠ p₁ →
p₂ ≠ p₃ →
p₁ ≠ p₃ →
2 • EuclideanGeometry.oangle p₃ p₁ s.center + 2 • EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi
This theorem is a result from Euclidean Geometry, specifically about the angles in certain isosceles triangles associated with a sphere. Given a normed additive commutative group `V`, an inner product space over `V` with real numbers, a metric space `P`, and a normed additive group with a torsor `P` over `V`. Assuming that the finite rank of `V` over `R` is 2 and `V` is an oriented module over `R`. Now, let `s` be a sphere in the Euclidean space and `p₁`, `p₂`, `p₃` be distinct points on the sphere `s`.
The theorem states that twice the base angle of an isosceles triangle with apex at the sphere's center, plus twice the angle at the apex of another triangle (which has the same base but with apex on the sphere), equals $\pi$ (pi). That is, $2 \cdot \text{angle}(p₃, p₁, \text{center}) + 2 \cdot \text{angle}(p₁, p₂, p₃) = \pi$.
More concisely: In a sphere in a Euclidean space with a 2-dimensional normed additive commutative group, the sum of twice the base angle and twice the angle at the apex of two isosceles triangles with the same base and apex on the sphere is equal to $\pi$.
|
EuclideanGeometry.cospherical_or_collinear_of_two_zsmul_oangle_eq
theorem EuclideanGeometry.cospherical_or_collinear_of_two_zsmul_oangle_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ : P},
2 • EuclideanGeometry.oangle p₁ p₂ p₄ = 2 • EuclideanGeometry.oangle p₁ p₃ p₄ →
EuclideanGeometry.Cospherical {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}
This theorem, named `EuclideanGeometry.cospherical_or_collinear_of_two_zsmul_oangle_eq`, states that in a 2-dimensional real inner product space, given four points `p₁`, `p₂`, `p₃` and `p₄`, if twice the oriented angle from `p₁` via `p₂` to `p₄` equals twice the oriented angle from `p₁` via `p₃` to `p₄`, then the set of these four points is either cospherical (i.e., all the points are equidistant from some other point) or collinear (i.e., they lie on the same straight line). This theorem is a converse of the geometric properties "angles in the same segment are equal" and "opposite angles of a cyclic quadrilateral add up to π", but with a conclusion of "cospherical or collinear" rather than equality of angles.
More concisely: In a 2-dimensional real inner product space, if the twice oriented angle between points `p₁`, `p₂`, and `p₄` equals the twice oriented angle between points `p₁`, `p₃`, and `p₄`, then the four points `p₁`, `p₂`, `p₃`, and `p₄` are either cospherical or collinear.
|
EuclideanGeometry.Sphere.oangle_center_eq_two_zsmul_oangle
theorem EuclideanGeometry.Sphere.oangle_center_eq_two_zsmul_oangle :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P},
p₁ ∈ s →
p₂ ∈ s →
p₃ ∈ s →
p₂ ≠ p₁ → p₂ ≠ p₃ → EuclideanGeometry.oangle p₁ s.center p₃ = 2 • EuclideanGeometry.oangle p₁ p₂ p₃
This theorem, named 'EuclideanGeometry.Sphere.oangle_center_eq_two_zsmul_oangle', proves a classical geometrical fact in the context of a sphere in Euclidean geometry. It asserts that for any sphere 's' in a two-dimensional inner product space over the reals and for any three distinct points 'p₁', 'p₂', 'p₃' on the sphere, the oriented angle at the sphere's center between the vectors from the center to 'p₁' and 'p₃' is twice the oriented angle between the vectors from 'p₁' to 'p₂' and from 'p₁' to 'p₃'. This is the well-known fact in plane geometry that the angle subtended by an arc at the center of a circle is twice the angle subtended by the same arc at any point on the circumference of the circle, generalized to spheres in higher dimensions.
More concisely: The oriented angle between the vector from a sphere's center to any two distinct points on the sphere is twice the oriented angle between the vectors from one point to the other.
|
EuclideanGeometry.Sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_left
theorem EuclideanGeometry.Sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_left :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
p₁ ∈ s →
p₂ ∈ s →
p₁ ≠ p₂ → EuclideanGeometry.oangle p₁ s.center p₂ = ↑Real.pi - 2 • EuclideanGeometry.oangle s.center p₂ p₁
This theorem states that in the context of Euclidean geometry, specifically in a 2-dimensional space modeled by an inner product space over the real numbers, the angle at the vertex of an isosceles triangle inscribed in a sphere is equal to the constant pi (π) minus twice the base angle. This base angle is considered in an oriented angle-at-a-point form where the vertex is taken as the center of the sphere. The points forming the isosceles triangle are subject to conditions that they are distinct and lie on the sphere. Here, the orientation of the 2-dimensional vector space and the measure of angles are carried out in accordance with the real numbers. The angles are expressed in terms of `EuclideanGeometry.oangle`, which represents an oriented angle between three points.
More concisely: In the context of Euclidean geometry, the angle at the center of an inscribed isosceles triangle in a sphere is equal to pi - 2 times the base angle.
|