Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-07 17:22 fcf0bfa8

View on Github →

feat(data/set/finite): add finite_to_set, finset.coe_to_finset

Estimated changes

Modified data/set/finite.lean

modified theorem finset.coe_filter

added theorem finset.coe_to_finset

added theorem finset.finite_to_set