Theorem MeasureTheory.stoppedValue_hitting_mem

Modification history

2024-11-04 23:02

Mathlib/Probability/Process/HittingTime.lean

chore(*): `LinearOrder` + `IsWellOrder α (· < ·)` → `LinearOrder` + `WellFoundedLT` (#18217) …

Modified MeasureTheory.stoppedValue_hitting_mem View on Github →

2023-06-19 04:18

Mathlib/Probability/Process/HittingTime.lean

feat: port Probability.Process.HittingTime (#5222)

Added MeasureTheory.stoppedValue_hitting_mem View on Github →