Theorem MeasureTheory.levyProkhorovEDist_le_of_forall_add_pos_le

Modification history

2024-02-17 14:51
Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
feat: Lévy-Prokhorov distance (#8719) …
Added MeasureTheory.levyProkhorovEDist_le_of_forall_add_pos_leView on Github →