Commit 2025-10-16 08:58 a03b1722
View on Github →chore: generalize Adapted to dependent types (#30549)
This PR generalizes Adapted to be a predicate about functions (i : ι) → Ω → β i instead of ι → Ω → β.
From the LeanBandits project, in which we have a sequence of random variables X 0, X 1, ... and want to says that n => (X_0, ..., X_n) is adapted to the natural filtration.