Commit 2025-06-08 08:19 3bb3ee2a

View on Github →

perf: replace measurability by fun_prop (#25577) Replace measurability by fun_prop where it made a visible difference in elaboration time.

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Countable.lean

Modified Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean

Modified Mathlib/Probability/Distributions/Geometric.lean

Modified Mathlib/Probability/Distributions/Poisson.lean

modified theorem ProbabilityTheory.measurable_poissonPMFReal