Commit 2022-01-24 12:47 f99af7da

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