Triangle congruence

This file proves the classical triangle congruence criteria for (possibly degenerate) triangles in real inner product spaces and Euclidean affine spaces. We prove SSS, SAS ASA, and AAS congruence.

Implementation notes

Side–Side–Side (SSS) congruence is proved using the definition of Congruent. Side–Angle–Side (SAS) congruence is proved via the law of cosines. Angle–Side–Angle (ASA) congruence is reduced to SAS using the law of sines. Angle–Angle–Side (AAS) congruence uses the fact that the sum of the angles in a triangle equals π, then reduces to ASA.

References

• https://en.wikipedia.org/wiki/Congruence_(geometry)

theorem EuclideanGeometry.triangle_congruent_iff_dist_eq {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)

theorem EuclideanGeometry.side_side_side {P₁ : Type u_4} {P₂ : Type u_5} [MetricSpace P₁] [MetricSpace P₂] {a b c : P₁} {a' b' c' : P₂} (hd₁ : dist a b = dist a' b') (hd₂ : dist b c = dist b' c') (hd₃ : dist c a = dist c' a') : Congruent ![a, b, c] ![a', b', c']

Side–Side–Side (SSS) congruence If all three corresponding sides of two triangles are equal, then the triangles are congruent. This holds even if the triangles are degenerate.

theorem EuclideanGeometry.side_angle_side {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₂] {a b c : P₁} {a' b' c' : P₂} (h : angle a b c = angle a' b' c') (hd₁ : dist a b = dist a' b') (hd₂ : dist b c = dist b' c') : Congruent ![a, b, c] ![a', b', c']

Side–Angle–Side (SAS) congruence If two triangles have two sides and the included angle equal, then the triangles are congruent. This holds even if the triangles are degenerate.

theorem EuclideanGeometry.angle_side_angle {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₂] {a b c : P₁} {a' b' c' : P₂} (h : ¬Collinear ℝ {a, b, c}) (ha₁ : angle a b c = angle a' b' c') (hd : dist b c = dist b' c') (ha₂ : angle b c a = angle b' c' a') : Congruent ![a, b, c] ![a', b', c']

Angle–Side–Angle (ASA) congruence If two triangles have two equal angles and the included side equal, then the triangles are congruent. We require that one of the triangles is non-degenerate, the non-collinearity of the other is then implied by the given equalities.

theorem EuclideanGeometry.angle_angle_side {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₂] {a b c : P₁} {a' b' c' : P₂} (h : ¬Collinear ℝ {a, b, c}) (ha₁ : angle a b c = angle a' b' c') (ha₂ : angle b c a = angle b' c' a') (hd : dist c a = dist c' a') : Congruent ![a, b, c] ![a', b', c']

Angle–Angle–Side (AAS) congruence If two triangles have two equal angles and a non-included side equal, then the triangles are congruent. We require that one of the triangles is non-degenerate, the non-collinearity of the other is then implied by the given equalities.

theorem EuclideanGeometry.angle_eq_of_congruent {ι : 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 : ι) : angle (v₁ i) (v₁ j) (v₁ k) = angle (v₂ i) (v₂ j) (v₂ k)

Corresponding angles are equal for congruent triangles.