triangle_congruent_iff_dist_eq — Mathlib

English

If the three corresponding sides of two triangles are equal, then the triangles are congruent (even if degenerate).

Русский

Если три соответствующие стороны двух треугольников равны, треугольники конгруэнтны (даже если они вырожденные).

LaTeX

$$$\text{If } dist(a,b)=dist(a',b'),\ dist(b,c)=dist(b',c'),\ dist(c,a)=dist(c',a')\text{ then } ![a,b,c] \cong ![a',b',c']$$$

Lean4

theorem triangle_congruent_iff_dist_eq {t₁ : Fin 3 → P₁} {t₂ : Fin 3 → P₂} :
    t₁ ≅ t₂ ↔ ∀ (i j : Fin 3), dist (t₁ i) (t₁ j) = dist (t₂ i) (t₂ j) :=
  congruent_iff_dist_eq

Похожие утверждения