Commit 2024-09-18 10:16 e9dae232

feat: rewrite cylinders and projective families of measures in terms of Finset.restrict (#16327) Rewrite cylinders and projective families of measures in terms of Finset.restrict. This avoids type ascription, and allows to rewrite a restriction as the composition of two restrictions, which is helpful when manipulating projective families.