Commit 2023-01-16 16:47 459a789a

View on Github →

feat: port Data.Finset.Option (#1596)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/Option.lean

added theorem Finset.card_insertNone

added theorem Finset.coe_eraseNone

added def Finset.eraseNone

added theorem Finset.eraseNone_empty

added theorem Finset.eraseNone_eq_bUnion

added theorem Finset.eraseNone_image_some

added theorem Finset.eraseNone_insert_none

added theorem Finset.eraseNone_inter

added theorem Finset.eraseNone_map_some

added theorem Finset.eraseNone_none

added theorem Finset.eraseNone_union

added theorem Finset.image_some_eraseNone

added def Finset.insertNone

added theorem Finset.insert_none_eraseNone

added theorem Finset.map_some_eraseNone

added theorem Finset.mem_eraseNone

added theorem Finset.mem_insertNone

added theorem Finset.some_mem_insertNone

added theorem Option.card_toFinset

added theorem Option.mem_toFinset

added def Option.toFinset

added theorem Option.toFinset_none

added theorem Option.toFinset_some