mathlib3

4eee8bc3 - chore(order/complete_lattice): Generalize `⨆`/`⨅` lemmas to dependent families (#13154)

chore(order/complete_lattice): Generalize `⨆`/`⨅` lemmas to dependent families (#13154) The "bounded supremum" and "bounded infimum" are both instances of nested `⨆`/`⨅`. But they only apply when the inner one runs over a predicate `p : ι → Prop`, and the function couldn't depend on `p`. This generalizes to `κ : ι → Sort*` and allows dependence on `κ i`. The lemmas are renamed from `bsupr`/`binfi` to `supr₂`/`infi₂` to show that they are more general. Some lemmas were missing between `⨆` and `⨅` or between `⨆`/`⨅` and nested `⨆`/`⨅`, so I'm adding them as well. Renames