Theorem MeasureTheory.hittingAfter_mono

Modification history

2025-11-24 13:11

Mathlib/Probability/Process/HittingTime.lean

feat: Monotonicity of hitting times (#31541) …

Added MeasureTheory.hittingAfter_mono View on Github →