Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-11 23:33 db305fb5

View on Github →

feat(data/set/finite): fintype_of_univ_finite (#6164) From lean-liquid

Estimated changes

Modified src/data/set/finite.lean

added def set.fintype_of_univ_finite

added theorem set.univ_finite_iff_nonempty_fintype