∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : OpensMeasurableSpace X]
  [CompletelyRegularSpace X] {x : X} (L : Filter X),
  Filter.Tendsto MeasureTheory.diracProba L (nhds (MeasureTheory.diracProba x)) ↔ Filter.Tendsto id L (nhds x)