Theorem MeasureTheory.tendsto_of_upcrossings_lt_top

Modification history

2026-09-21 19:06
Mathlib/Probability/Martingale/Convergence.lean
chore: rename declarations whose names do not match their statements (#44051) …
Added MeasureTheory.tendsto_of_upcrossings_lt_topView on Github →