mathlib3

764d7a90 - feat(probability/stopping): first hitting time (#14630)

feat(probability/stopping): first hitting time (#14630) This PR adds the first hitting time (before some time) and proves that it is a stopping time in the discrete case. Co-authored-by: RemyDegenne <Remydegenne@gmail.com>