Theorems · Theorem · general topology

Set.infsep_triple

∀ {α : Type u_1} [inst : PseudoMetricSpace α] {x y z : α},
  x ≠ y → y ≠ z → x ≠ z → {x, y, z}.infsep = min (min (dist x y) (dist x z)) (dist y z)

Defined in

Mathlib.Topology.MetricSpace.Infsep

Cited by

0 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace