Commit 2025-08-22 22:36 7b26cbd9
View on Github →chore(MeasureTheory/Measure): deprecate injective_diracProba_of_T0 (duplicate) (#28491)
The typeclass hypotheses of injective_diracProba_of_T0 imply those of injective_diracProba via separatesPointsOfOpensMeasurableSpaceOfT0Space.