Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-03-15 00:57 f7977ff5

View on Github →

feat(data/finset): add finset.powerset

Estimated changes

Modified data/finset.lean

added theorem finset.card_powerset

added theorem finset.empty_mem_powerset

added theorem finset.mem_powerset

added theorem finset.mem_powerset_self

added def finset.powerset

added theorem finset.powerset_mono

Modified data/list/basic.lean

added theorem list.length_sublists'

modified theorem list.length_sublists

added theorem list.map_sublists'_aux

added theorem list.mem_sublists'

modified theorem list.nodup_map

added theorem list.nodup_map_iff

added theorem list.nodup_sublists'

added theorem list.pairwise_sublists'

modified theorem list.pairwise_sublists

added theorem list.reverse_injective

added def list.sublists'

added def list.sublists'_aux

added theorem list.sublists'_aux_append

added theorem list.sublists'_aux_eq_sublists'

added theorem list.sublists'_cons

added theorem list.sublists'_eq_sublists

added theorem list.sublists'_nil

added theorem list.sublists'_reverse

added theorem list.sublists'_singleton

added theorem list.sublists_eq_sublists'

added theorem list.sublists_reverse

Modified data/list/perm.lean

added theorem list.perm_ext_sublist_nodup

added theorem list.sublists_cons_perm_append

added theorem list.sublists_perm_sublists'

Modified data/multiset.lean

added theorem multiset.card_powerset

added theorem multiset.map_single_le_powerset

added theorem multiset.mem_powerset

added theorem multiset.nodup_powerset

modified def multiset.pmap

added def multiset.powerset

added def multiset.powerset_aux'

added theorem multiset.powerset_aux'_cons

added theorem multiset.powerset_aux'_nil

added theorem multiset.powerset_aux'_perm

added def multiset.powerset_aux

added theorem multiset.powerset_aux_eq_map_coe

added theorem multiset.powerset_aux_perm

added theorem multiset.powerset_aux_perm_powerset_aux'

added theorem multiset.powerset_coe'

added theorem multiset.powerset_coe