51 Geometry

TheoremApollonius's theorem#

Apollonius's Theorem.

EuclideanGeometry.dist_sq_add_dist_sq_eq_two_mul_dist_midpoint_sq_add_half_dist_sq.{u_1, u_2}
  {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
  [NormedAddTorsor V P] (a b c : P) :
  dist a b ^ 2 + dist a c ^ 2 = 2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2)
Sources
MathlibEuclideanGeometry.dist_sq_add_dist_sq_eq_two_mul_dist_midpoint_sq_add_half_dist_sq
Uses 8
Statement usesAffine function · Characteristic zero · Euclidean affine space · Field \(\R\) of real numbers · Inner product space, over \(R\) or \(C\) · Invertible elements
Proof usesOrdered ring · Stewart's theorem

TheoremBritish flag theorem#

British flag theorem: for a rectangle a b c d and any point p (not necessarily in the plane of the rectangle), the sum of the squares of the distances from p to the opposite corners a and c equals the sum of the squares of the distances from p to b and d.

EuclideanGeometry.dist_sq_add_dist_sq_eq_dist_sq_add_dist_sq_of_angle_eq_pi_div_two.{u_1, u_2}
  {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
  [NormedAddTorsor V P] {a b c d : P} (h : midpoint ℝ a c = midpoint ℝ b d)
  (ha : EuclideanGeometry.angle b a d = Real.pi / 2) (p : P) :
  dist p a ^ 2 + dist p c ^ 2 = dist p b ^ 2 + dist p d ^ 2
Sources
MathlibEuclideanGeometry.dist_sq_add_dist_sq_eq_dist_sq_add_dist_sq_of_angle_eq_pi_div_two
Uses 5
Statement usesAffine function · Angle · Characteristic zero · Euclidean affine space · Invertible elements

TheoremCommandino's theorem#

Commandino's theorem : For n-simplex, the vector from a vertex to the centroid equals n times the vector from the centroid to the corresponding faceOppositeCentroid.

Affine.Simplex.point_vsub_centroid_eq_smul_vsub.{u_1, u_2, u_3} {k : Type u_1} {V : Type u_2}
  {P : Type u_3} [DivisionRing k] [AddCommGroup V] [_root_.Module k V] [AddTorsor V P] {n : ℕ}
  [NeZero n] [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)) :
  s.points i -ᵥ s.centroid = ↑n • (s.centroid -ᵥ s.faceOppositeCentroid i)
Sources
MathlibAffine.Simplex.point_vsub_centroid_eq_smul_vsub
Uses 3
Statement usesBarycenter · Characteristic zero · Rational number

TheoremCPCTC#

Mathlib records this with 2 declarations.

EuclideanGeometry.triangle_congruent_iff_dist_eq.

EuclideanGeometry.triangle_congruent_iff_dist_eq.{u_4, u_5} {P₁ : Type u_4} {P₂ : Type u_5}
  [MetricSpace P₁] [MetricSpace P₂] {t₁ : Fin 3 → P₁} {t₂ : Fin 3 → P₂} :
  Congruent t₁ t₂ ↔ ∀ (i j : Fin 3), dist (t₁ i) (t₁ j) = dist (t₂ i) (t₂ j)

EuclideanGeometry.angle_eq_of_congruent: Corresponding angles are equal for congruent triangles.

EuclideanGeometry.angle_eq_of_congruent.{u_1, u_2, u_3, u_4, u_5} {ι : Type u_1} {V₁ : Type u_2}
  {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [NormedAddCommGroup V₁] [NormedAddCommGroup V₂]
  [InnerProductSpace ℝ V₁] [InnerProductSpace ℝ V₂] [MetricSpace P₁] [MetricSpace P₂]
  [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] {v₁ : ι → P₁} {v₂ : ι → P₂} (h : Congruent v₁ v₂)
  (i j k : ι) :
  EuclideanGeometry.angle (v₁ i) (v₁ j) (v₁ k) = EuclideanGeometry.angle (v₂ i) (v₂ j) (v₂ k)
Sources
MathlibEuclideanGeometry.triangle_congruent_iff_dist_eq · EuclideanGeometry.angle_eq_of_congruent
Uses 2
Statement usesAngle · Euclidean affine space

TheoremExterior angle theorem#

The Exterior angle theorem. an exterior angle of a triangle is equal to the sum of the measures of the remote interior angles.

EuclideanGeometry.exterior_angle_eq_angle_add_angle.{u_1, u_2} {V : Type u_1} {P : Type u_2}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P]
  {p₁ p₂ p₃ : P} (p : P) (h : Sbtw ℝ p p₁ p₂) :
  EuclideanGeometry.angle p₃ p₁ p =
    EuclideanGeometry.angle p₁ p₃ p₂ + EuclideanGeometry.angle p₃ p₂ p₁
Sources
MathlibEuclideanGeometry.exterior_angle_eq_angle_add_angle
Uses 4
Statement usesAffine function · Angle · Euclidean affine space
Proof usesSum of the Angles of a Triangle

TheoremGeometric mean theorem#

Geometric mean theorem (or right triangle altitude theorem): in a right-angled triangle p₁ p₂ p₃ with the right angle at p₂, the square of the altitude dist p₂ p₄ to the hypotenuse is the product of the two segments dist p₁ p₄ and dist p₃ p₄ into which its foot p₄ divides the hypotenuse.

EuclideanGeometry.dist_sq_eq_dist_mul_dist_of_angle_eq_pi_div_two.{u_1, u_2} {V : Type u_1}
  {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
  [NormedAddTorsor V P] {p₁ p₂ p₃ p₄ : P} (hf : Sbtw ℝ p₁ p₄ p₃)
  (hc : EuclideanGeometry.angle p₁ p₄ p₂ = Real.pi / 2)
  (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) : dist p₂ p₄ ^ 2 = dist p₁ p₄ * dist p₃ p₄
Sources
MathlibEuclideanGeometry.dist_sq_eq_dist_mul_dist_of_angle_eq_pi_div_two
Uses 3
Statement usesAffine function · Angle · Euclidean affine space

TheoremIntersecting secants theorem#

Intersecting Secants Theorem.

EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero.{u_1, u_2} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P]
  [NormedAddTorsor V P] {a b c d p : P} (h : EuclideanGeometry.Cospherical {a, b, c, d})
  (hab : a ≠ b) (hcd : c ≠ d) (hapb : EuclideanGeometry.angle a p b = 0)
  (hcpd : EuclideanGeometry.angle c p d = 0) : dist a p * dist b p = dist c p * dist d p
Sources
MathlibEuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero
Uses 9
Statement usesAngle · Euclidean affine space
Proof usesAffine function · Affine span · Cardinal · Characteristic zero · Invertible elements · Linear independence · Ordered ring

TheoremStewart's theorem#

Stewart's Theorem.

EuclideanGeometry.dist_sq_mul_dist_add_dist_sq_mul_dist.{u_1, u_2} {V : Type u_1} {P : Type u_2}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (a b c p : P)
  (h : EuclideanGeometry.angle b p c = Real.pi) :
  dist a b ^ 2 * dist c p + dist a c ^ 2 * dist b p =
    dist b c * (dist a p ^ 2 + dist b p * dist c p)
Sources
MathlibEuclideanGeometry.dist_sq_mul_dist_add_dist_sq_mul_dist
Uses 3 · Used by 2
Statement usesAngle · Euclidean affine space
Proof usesThe Law of Cosines
Used byPtolemy’s Theorem · Apollonius's theorem

TheoremTangent-secant theorem#

Tangent-Secant Theorem. The square of the tangent length equals the product of secant segment lengths.

EuclideanGeometry.Sphere.dist_sq_eq_mul_dist_of_tangent_and_secant.{u_1, u_2} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P]
  [NormedAddTorsor V P] {a b t p : P} {s : EuclideanGeometry.Sphere P} (ha : a ∈ s) (hb : b ∈ s)
  (hp : p ∈ line[ℝ, a, b]) (h_tangent : s.IsTangentAt t line[ℝ, p, t]) :
  dist p t ^ 2 = dist p a * dist p b
Sources
MathlibEuclideanGeometry.Sphere.dist_sq_eq_mul_dist_of_tangent_and_secant
Uses 8
Statement usesAffine span · Euclidean affine space · Orthogonal complement
Proof usesAffine function · Angle · Characteristic zero · Invertible elements · Ordered ring

TheoremThales's theorem#

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.

EuclideanGeometry.Sphere.thales_theorem.{u_1, u_2} {V : Type u_1} {P : Type u_2}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P]
  {p₁ p₂ p₃ : P} {s : EuclideanGeometry.Sphere P} (hd : s.IsDiameter p₁ p₃) :
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 ↔ p₂ ∈ s
Sources
MathlibEuclideanGeometry.Sphere.thales_theorem
Uses 6
Statement usesAffine function · Angle · Characteristic zero · Euclidean affine space · Invertible elements
Proof usesOrdered ring

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.