powersetCard_le_powerset — Mathlib

English

For all n and s, powersetCard n s is a submultiset of powerset s.

Русский

Для всех n и s, powersetCard n s является подмножством powerset s.

LaTeX

$$$\mathrm{powersetCard}\ n\ s \le \mathrm{powerset}(s)$$$

Lean4

theorem powersetCard_le_powerset (n : ℕ) (s : Multiset α) : powersetCard n s ≤ powerset s :=
  Quotient.inductionOn s fun l =>
    by
    simp only [quot_mk_to_coe, powersetCard_coe, powerset_coe', coe_le]
    exact ((sublistsLen_sublist_sublists' _ _).map _).subperm

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