mathlib

1be91a1b - chore(order/filter/lift,topology/algebra/ordered): drop `[nonempty ι]` (#6861)

chore(order/filter/lift,topology/algebra/ordered): drop `[nonempty ι]` (#6861) * add `set.powerset_univ`, `filter.lift_top`, `filter.lift'_top`; * remove `[nonempty ι]` from `filter.lift'_infi_powerset` and `tendsto_Icc_class_nhds_pi`.