# Commit 2022-01-24 12:47 f99af7da

View on Github →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