Theorems · Theorem · general topology

IsUltrametricDist.dist_eq_max_of_dist_ne_dist

∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] (x y z : X),
  dist x y ≠ dist y z → dist x z = max (dist x y) (dist y z)

All triangles are isosceles in an ultrametric space.

Defined in

Mathlib.Topology.MetricSpace.Ultra.Basic

Cited by

2 results in Mathlib

Foundations

Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpaceIsUltrametricDist