Theorem Multiset.powerset_le_powerset_iff_le

Modification history

2026-03-10 20:04
Mathlib/Data/Multiset/Powerset.lean
feat(Data/Multiset/Powerset): show injectivity and monotonicity of powerset (#35465) …
Added Multiset.powerset_le_powerset_iff_leView on Github →