Commit 2025-10-17 14:39 9823cfe9
View on Github →chore: generalize Egorov file to measurable edist assumption (#30604)
This PR generalizes the lemmas of the Egorov theorem file to use measurability of distances instead of strong measurability of the processes.
For the proof of the Kolmogorov-Chentsov theorem in the Brownian process project, we don't have strong measurability of the processes but we have measurability of the distances and we want to use an equivalent of tendstoInMeasure_of_tendsto_ae.