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