Theorems · Theorem · geometry

EuclideanGeometry.side_side_side

∀ {P₁ : Type u_4} {P₂ : Type u_5} [inst : MetricSpace P₁] [inst_1 : MetricSpace P₂] {a b c : P₁} {a' b' c' : P₂},
  dist a b = dist a' b' → dist b c = dist b' c' → 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.

Defined in

Mathlib.Geometry.Euclidean.Congruence

Cited by

1 results in Mathlib

Foundations

Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MetricSpaceMetricSpace