English
The distance satisfies ultrametric triangle inequality: dist(x,z) ≤ max(dist(x,y), dist(y,z)).
Русский
Расстояние удовлетворяет ультраметрическое неравенство треугольника: dist(x,z) ≤ max(dist(x,y), dist(y,z)).
LaTeX
$$$$ \operatorname{dist}(x,z) \le \max\bigl(\operatorname{dist}(x,y), \operatorname{dist}(y,z)\bigr) $$$$
Lean4
theorem dist_triangle_nonarch (x y z : ∀ n, E n) : dist x z ≤ max (dist x y) (dist y z) :=
by
rcases eq_or_ne x z with (rfl | hxz)
· simp [PiNat.dist_self x, PiNat.dist_nonneg]
rcases eq_or_ne x y with (rfl | hxy)
· simp
rcases eq_or_ne y z with (rfl | hyz)
· simp
simp only [dist_eq_of_ne, hxz, hxy, hyz, inv_le_inv₀, one_div, inv_pow, zero_lt_two, Ne, not_false_iff, le_max_iff,
pow_le_pow_iff_right₀, one_lt_two, pow_pos, min_le_iff.1 (min_firstDiff_le x y z hxz)]
