Commit 2025-02-13 10:15 7f7be12e

View on Github →

feat: more measurability for updateFinset (#21796) updateFinset is measurable with respect to both arguments.

Estimated changes

modified theorem measurable_updateFinset