mathlib3

f99af7da - chore(data/set/lattice): Generalize more `⋃`/`⋂` lemmas to dependent families (#11516)

chore(data/set/lattice): Generalize more `⋃`/`⋂` lemmas to dependent families (#11516) The "bounded union" and "bounded intersection" are both instances of nested `⋃`/`⋂`. But they only apply when the inner one runs over a predicate `p : ι → Prop`, and the resulting set couldn't depend on `p`. This generalizes to `κ : ι → Sort*` and allows dependence on `κ i`. The lemmas are renamed from `bUnion`/`bInter` to `Union₂`/`Inter₂` to show that they are more general. Some generalizations lead to unification problems, so I've kept the `b` version around. Some lemmas were missing between `⋃` and `⋂` or between `⋃`/`⋂` and nested `⋃`/`⋂`, so I'm adding them as well. Renames