dist_triangle — Mathlib

English

The upper-half-plane distance satisfies the triangle inequality: dist(a,c) ≤ dist(a,b) + dist(b,c).

Русский

Расстояние в верхней полуплоскости удовлетворяет треугольному неравенству: dist(a,c) ≤ dist(a,b) + dist(b,c).

LaTeX

$$$dist(a,c) ≤ dist(a,b) + dist(b,c)$$$

Lean4

protected theorem dist_triangle (a b c : ℍ) : dist a c ≤ dist a b + dist b c :=
  by
  rw [dist_le_iff_le_sinh, sinh_half_dist_add_dist, div_mul_eq_div_div _ _ (dist _ _), le_div_iff₀, div_mul_eq_mul_div]
  · gcongr
    exact EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist (a : ℂ) b c (conj (b : ℂ))
  · rw [dist_comm, dist_pos, Ne, Complex.conj_eq_iff_im]
    exact b.im_ne_zero

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