mathlib
34cfcd02 - feat(probability/stopping): generalize `is_stopping_time.measurable_set_lt` and variants beyond `ℕ` (#12240)

Commit
3 years ago
feat(probability/stopping): generalize `is_stopping_time.measurable_set_lt` and variants beyond `ℕ` (#12240) The lemma `is_stopping_time.measurable_set_lt` and the similar results for gt, ge and eq were written for stopping times with value in nat. We generalize those results to linear orders with the order topology.
Author
Parents
Loading