Commit 2026-03-10 20:04 d5a55b51

View on Github →

feat(Data/Multiset/Powerset): show injectivity and monotonicity of powerset (#35465) Add Injective, Monotone, and StrictMono proofs for Multiset.powerset. Also, add a theorem showing that the sizes of two powersets are bidirectionally related to the sizes of the underlying Multisets (powerset_le_powerset_iff_le), a couple of other small Multiset.powerset lemmas, and theorems for append and map for List.Subperm. Also, thanks to Ruben Van de Velde for looking this over on the Zulip!

Estimated changes

Modified Mathlib/Data/List/Perm/Subperm.lean

added theorem List.Subperm.append

added theorem List.map_subperm_map_iff

Modified Mathlib/Data/List/Sublists.lean

added theorem List.Sublist.sublists'

added theorem List.sublists'_sublist_sublists'_iff

added theorem List.subperm_of_sublists'_subperm_sublists'

Modified Mathlib/Data/Multiset/Powerset.lean

added theorem Multiset.powerset_eq_singleton_zero_iff

added theorem Multiset.powerset_injective

added theorem Multiset.powerset_le_powerset_iff_le

added theorem Multiset.powerset_mono

added theorem Multiset.powerset_strictMono

added theorem Multiset.self_mem_powerset

added theorem Multiset.zero_mem_powerset