Commit 2022-05-06 12:03 e4d3d339

feat(probability/stopping): add properties of the measurable space generated by a stopping time (#13909)

• add lemmas stating that various sets are measurable with respect to that space
• describe the sigma algebra generated by the minimum of two stopping times
• use the results to generalize is_stopping_time.measurable_set_eq_const from nat to first countable linear orders and rename it to is_stopping_time.measurable_space_eq' to have a name similar to is_stopping_time.measurable_set_eq.