Theorems · Theorem · general topology

Set.einfsep_triple

∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {x y z : α},
  x ≠ y → y ≠ z → x ≠ z → {x, y, z}.einfsep = min (min (edist x y) (edist x z)) (edist y z)

Defined in

Mathlib.Topology.MetricSpace.Infsep

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpace