Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-25 15:21 1be91a1b

View on Github →

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.

Estimated changes

added theorem set.powerset_univ
modified theorem filter.lift'_infi_powerset
added theorem filter.lift'_top
added theorem filter.lift_top