Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-06 16:48 e5c4eb1b

View on Github →

feat(data/set): add lift converting finset to set

Estimated changes

Modified data/set/default.lean

Modified data/set/finite.lean

added theorem finset.coe_bind

added theorem finset.coe_empty

added theorem finset.coe_eq_coe

added theorem finset.coe_erase

added theorem finset.coe_filter

added theorem finset.coe_image

added theorem finset.coe_insert

added theorem finset.coe_inter

added theorem finset.coe_sdiff

added theorem finset.coe_singleton

added theorem finset.coe_subseteq_coe

added theorem finset.coe_union

added theorem finset.mem_coe

added def finset.to_set