∀ {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  (s t : MeasureTheory.MeasuredSets μ), edist s t = ENNReal.ofReal ((fun s t => μ.real (symmDiff ↑s ↑t)) s t)