Commit 2025-12-12 15:51 e944d995

feat: FiniteExhaustion (#31921) Creates a structure that contains the data of a non-decreasing sequence of finite sets whose union equals some countable set. This is used in the brownian motion project to transfer a theorem that holds over finite sets to a countable set (with monotone convergence). The design is modelled on CompactExhaustion (of course it can be seen as precisely a special case but I think taking that approach would be much more convoluted). I didn't want to give this its own file, but I couldn't put it in Mathlib.Data.Set.Countable without creating a large-import because I needed the fact that product of finite sets is finite, and couldn't find anywhere else sensible to put it that wouldn't create a large-import. Would be happy if someone has a better suggestion.