Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-05 17:22 2adc122c

View on Github →

feat(data/set/finite): remove exists_finset_of_finite (#1782)

  • feat(data/set/finite): remove exists_finset_of_finite exists_finset_of_finite is a duplicate of finite.exists_finset_coe At same time, provide a can_lift instance to lift sets to finsets.
  • Add docstring

Estimated changes