map_single_le_powerset — Mathlib

English

For any multiset s, the multiset consisting of all singleton submultisets of s is less than or equal to the powerset of s.

Русский

Для любого мультимножества s множество, состоящее из одиночных подмультимножеств s, вкладывается в powerset(s).

LaTeX

$$$ \\mathrm{map}(\\mathrm{singleton})(s) \\le \\mathrm{powerset}(s) $$$

Lean4

theorem map_single_le_powerset (s : Multiset α) : s.map singleton ≤ powerset s :=
  Quotient.inductionOn s fun l =>
    by
    simp only [powerset_coe, quot_mk_to_coe, coe_le, map_coe]
    change l.map (((↑) : List α → Multiset α) ∘ pure) <+~ (sublists l).map (↑)
    rw [← List.map_map]
    exact ((map_pure_sublist_sublists _).map _).subperm

Похожие утверждения