mathlib

b8c3e61b - refactor(*): Use `finset.Iix`/`finset.Ixi` (#14448)

refactor(*): Use `finset.Iix`/`finset.Ixi` (#14448) Now that `finset.Iix`/`finset.Ixi` work for empty types, there is no need for `univ.filter (λ j, j < i)` and similar.