mathlib

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

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`.