powersetCard_one — Mathlib

English

The 1-element submultisets of s are exactly the singleton multisets formed from each element of s.

Русский

Подмножества размера 1 множества s равны все одноэлементные подмножества, полученные из каждого элемента s.

LaTeX

$$$\mathrm{powersetCard}(1,s) = s.map\,\mathrm{singleton}$$$

Lean4

theorem powersetCard_one (s : Multiset α) : powersetCard 1 s = s.map singleton :=
  Quotient.inductionOn s fun l ↦ by simp [powersetCard_coe, sublistsLen_one, map_reverse, Function.comp_def]

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