Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-22 18:11 1f0096e6

View on Github →

refactor(data/set/finite): reduce imports (#18245)

  • Add eq_or_eq_or_eq_of_forall_not_lt_lt, finite.of_forall_not_lt_lt, set.finite_of_forall_not_lt_lt (replacing set.finite_of_forall_between_eq_endpoints), and set.finite_of_forall_not_lt_lt'.
  • Import data.finset.basic instead of data.finset.sort in data.set.finite.
  • Forward-ported in leanprover-community/mathlib4#1738

Estimated changes