dist_triangle8 — Mathlib

English

For all a,b,c,d,e,f,g,h ∈ α, dist(a,h) ≤ dist(a,b) + dist(b,c) + dist(c,d) + dist(d,e) + dist(e,f) + dist(f,g) + dist(g,h).

Русский

Для любых a,b,c,d,e,f,g,h ∈ α верно: dist(a,h) ≤ dist(a,b) + dist(b,c) + dist(c,d) + dist(d,e) + dist(e,f) + dist(f,g) + dist(g,h).

LaTeX

$$$dist(a,h) \le dist(a,b) + dist(b,c) + dist(c,d) + dist(d,e) + dist(e,f) + dist(f,g) + dist(g,h)$$$

Lean4

theorem dist_triangle8 (a b c d e f g h : α) :
    dist a h ≤ dist a b + dist b c + dist c d + dist d e + dist e f + dist f g + dist g h :=
  by
  apply le_trans (dist_triangle4 a f g h)
  gcongr
  apply le_trans (dist_triangle4 a d e f)
  gcongr
  exact dist_triangle4 a b c d

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