Commit 2026-02-15 07:46 a51d653d

View on Github →

feat: generalize IsStoppingTime.add (#34912) IsStoppingTime.add is originally proved only for ℕ. This PR proves the same theorem for a countable linearly ordered set ι that is CanonicallyOrderedAdd and equppied with the order topology.

Estimated changes

Modified Mathlib/Probability/Process/Stopping.lean

modified theorem MeasureTheory.IsStoppingTime.add

added theorem MeasureTheory.IsStoppingTime.add_const'

deleted theorem MeasureTheory.IsStoppingTime.add_const_nat