sup_powerset_len — Mathlib

English

For a multiset x, the supremum over k of the powerset-card of x at level k equals x.powerset, i.e., the powerset size is reached by the supremum construction.

Русский

Для мультисемейства x, верхняя граница по уровню k мощности множества равно x.powerset.

LaTeX

$$$\operatorname{sup}_{k=0}^{|x|} (|x|\text{-powerset-card}(k)) = |x|\text{-powerset}$$$

Lean4

theorem sup_powerset_len [DecidableEq α] (x : Multiset α) :
    (Finset.sup (Finset.range (card x + 1)) fun k => x.powersetCard k) = x.powerset :=
  by
  convert bind_powerset_len x using 1
  rw [Multiset.bind, Multiset.join, ← Finset.range_val, ← Finset.sum_eq_multiset_sum]
  exact Eq.symm (finset_sum_eq_sup_iff_disjoint.mpr fun _ _ _ _ h => pairwise_disjoint_powersetCard x h)

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