English
The power set of s is the disjoint union, over i from 0 to |s|, of powersetCard i s.
Русский
Множество подмножеств P(s) разбивается на попарно непересекающиеся части по размерности i = 0,...,|s|, где каждая часть равна powersetCard i s.
LaTeX
$$Finset.powerset(s) = (range (s.card + 1)).disjiUnion (fun i => powersetCard i s) (s.pairwise_disjoint_powersetCard.set_pairwise _)$$
Lean4
theorem powerset_card_disjiUnion (s : Finset α) :
Finset.powerset s =
(range (s.card + 1)).disjiUnion (fun i => powersetCard i s) (s.pairwise_disjoint_powersetCard.set_pairwise _) :=
by
refine ext fun a => ⟨fun ha => ?_, fun ha => ?_⟩
· rw [mem_disjiUnion]
exact
⟨a.card, mem_range.mpr (Nat.lt_succ_of_le (card_le_card (mem_powerset.mp ha))),
mem_powersetCard.mpr ⟨mem_powerset.mp ha, rfl⟩⟩
· rcases mem_disjiUnion.mp ha with ⟨i, _hi, ha⟩
exact mem_powerset.mpr (mem_powersetCard.mp ha).1
