English
In an ultrametric space, if d(x,y) ≠ d(y,z), then d(x,z) = max(d(x,y), d(y,z)).
Русский
В ультраметрическом пространстве если d(x,y) ≠ d(y,z), то d(x,z) = max{d(x,y), d(y,z)}.
LaTeX
$$(\operatorname{dist}(x,y) \neq \operatorname{dist}(y,z)) \Rightarrow \operatorname{dist}(x,z) = \max\bigl(\operatorname{dist}(x,y), \operatorname{dist}(y,z)\bigr)$$
Lean4
/-- All triangles are isosceles in an ultrametric space. -/
theorem dist_eq_max_of_dist_ne_dist (h : dist x y ≠ dist y z) : dist x z = max (dist x y) (dist y z) :=
by
apply le_antisymm (dist_triangle_max x y z)
rcases h.lt_or_gt with h | h
· rw [max_eq_right h.le]
apply (le_max_iff.mp <| dist_triangle_max y x z).resolve_left
simpa only [not_le, dist_comm x y] using h
· rw [max_eq_left h.le, dist_comm x y, dist_comm x z]
apply (le_max_iff.mp <| dist_triangle_max y z x).resolve_left
simpa only [not_le, dist_comm x y] using h
