Public Mathlib landmark · existing upstream theorem · read-only
ProofAtlas

Geometry · existing Mathlib declaration

Thales’ Theorem

Fix a sphere and two points already known to be endpoints of one of its diameters. For any point p₂, the angle from the first endpoint through p₂ to the other endpoint is a right angle if and only if p₂ lies on the sphere.

The theorem at a glance

Thales’ Theorem at a glance

A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.

For fixed diameter endpoints p₁ and p₃, a point p₂ lies on the sphere if and only if the angle at p₂ is π/2. Generated explanation only; the exact HTML statement and pinned source are authoritative.
Detailed visual description

The poster pairs the exact equivalence with a single spherical boundary: p₁ and p₃ are antipodal endpoints of a centered diameter, p₂ lies on the same boundary, and its two chords meet at a right-angle marker. The footer preserves the arbitrary real inner-product affine-space scope and the absence of distinctness or positive-radius hypotheses.

Formal orientation

Statement map

Statement map for Thales’ TheoremGiven two endpoints of a diameter of a sphere in a real inner-product affine space, the angle they subtend at a point is right exactly when that point lies on the sphere. The pinned upstream declaration is EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter. The exact checked statement is theorem EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} {s : EuclideanGeometry.Sphere P} (hd : s.IsDiameter p₁ p₃) : ∠ p₁ p₂ p₃ = π / 2 ↔ p₂ ∈ s.Mathematical readingGiven two endpoints of adiameter of a sphere ina real inner-productaffine space, the anglethey subtend at a pointis right exactly whenthat point lies on thesphere.Pinned declarationmathlib ·EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameterExact checked formtheoremEuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter{V : Type*} {P : Type*}[NormedAddCommGroup V][InnerProductSpace ℝ V][MetricSpace P][NormedAddTorsor V P]{p₁ p₂ p₃ : P} {s :EuclideanGeometry.SphereP} (hd : s.IsDiameter p₁p₃) : ∠ p₁ p₂ p₃ = π / 2↔ p₂ ∈ sStatement map for Thales’ TheoremGiven two endpoints of a diameter of a sphere in a real inner-product affine space, the angle they subtend at a point is right exactly when that point lies on the sphere. The pinned upstream declaration is EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter. The exact checked statement is theorem EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} {s : EuclideanGeometry.Sphere P} (hd : s.IsDiameter p₁ p₃) : ∠ p₁ p₂ p₃ = π / 2 ↔ p₂ ∈ s.Mathematical readingGiven two endpoints of adiameter of a sphere ina real inner-productaffine space, the anglethey subtend at a pointis right exactly whenthat point lies on thesphere.Pinned declarationmathlib ·EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameterExact checked formtheoremEuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter{V : Type*} {P : Type*}[NormedAddCommGroup V][InnerProductSpace ℝ V][MetricSpace P][NormedAddTorsor V P]{p₁ p₂ p₃ : P} {s :EuclideanGeometry.SphereP} (hd : s.IsDiameter p₁p₃) : ∠ p₁ p₂ p₃ = π / 2↔ p₂ ∈ s

This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.

With p₁ and p₃ fixed as diameter endpoints, the angle at p₂ is right exactly when p₂ lies on the sphere. Scientific diagram · explanatory, not proof evidence.
Detailed visual description

This page indexes Mathlib’s theorem for a metric affine space P modeled on a real inner-product space V. Once s.IsDiameter p₁ p₃ is given, the declaration proves ∠p₁p₂p₃ = π/2 if and only if p₂ ∈ s. It has no dimension-two, pairwise-distinctness, or positive-radius hypothesis. A planar great-circle picture is an illustrative cross-section, not the theorem’s full scope. The selected declaration does not prove the nearby two-dimensional result that recovers a diameter from three points already lying on an arbitrary sphere.

Complementary intuition

A mathematical landmark

Thales’ theorem is a foundational bridge between incidence and orthogonality. Mathlib states the result as an exact two-way sphere-membership equivalence in an arbitrary real inner-product affine space, and its proof exposes the inner-product identity behind the familiar great-circle picture.

The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.

Authoritative formal type

Exact Mathlib statement

theorem EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} {s : EuclideanGeometry.Sphere P} (hd : s.IsDiameter p₁ p₃) : ∠ p₁ p₂ p₃ = π / 2 ↔ p₂ ∈ s
Selected evidence declaration text
theorem EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} {s : EuclideanGeometry.Sphere P} (hd : s.IsDiameter p₁ p₃) : ∠ p₁ p₂ p₃ = π / 2 ↔ p₂ ∈ s

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally
Locally reproducedExact upstream declaration replayed
Reviewed pageCurrent public presentation reviewed
Accepted Atlas resultNot recorded for the preferred artifact

These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.

Claim boundary

No new theorem is claimed

This page indexes Mathlib’s theorem for a metric affine space P modeled on a real inner-product space V. Once s.IsDiameter p₁ p₃ is given, the declaration proves ∠p₁p₂p₃ = π/2 if and only if p₂ ∈ s. It has no dimension-two, pairwise-distinctness, or positive-radius hypothesis. A planar great-circle picture is an illustrative cross-section, not the theorem’s full scope. The selected declaration does not prove the nearby two-dimensional result that recovers a diameter from three points already lying on an arbitrary sphere.

Provenance

Origin and evidence stay separate

Existing declaration
EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter in mathlib
Relationship
The checked artifact is the upstream declaration itself
Preferred checked artifact
artifact.library.mathlib.thales-theorem.v001
Source handling
Verified upstream reference; no mirrored source package