powerset_card_biUnion — Mathlib

English

Equivalent formulation: powerset s is the disjoint union of powersetCard i s as i ranges up to card s.

Русский

Эквивалентная формулировка: powerset s является попарно непересекающимся объединением powersetCard i s при i от 0 до card s.

LaTeX

$$Finset.powerset s = (range (s.card + 1)).disjiUnion (fun i => Finset.powersetCard i s) (s.pairwise_disjoint_powersetCard.set_pairwise _)$$

Lean4

theorem powerset_card_biUnion [DecidableEq (Finset α)] (s : Finset α) :
    Finset.powerset s = (range (s.card + 1)).biUnion fun i => powersetCard i s := by
  simpa only [disjiUnion_eq_biUnion] using powerset_card_disjiUnion s

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