English
Let s be a finite set and a an element. The power set of insert a s equals the union of the power set of s and the image, under insertion of a, of the power set of s.
Русский
Пусть s — конечное множество и a — элемент. Множество подмножеств {a} ∪ s равно объединению подмножеств s и изображения подмножеств s, полученного добавлением a.
LaTeX
$$$\operatorname{powerset}(\operatorname{insert}(a,s)) = \operatorname{powerset}(s) \cup \operatorname{powerset}(s).image(\operatorname{insert}(a))$$$
Lean4
theorem powerset_insert [DecidableEq α] (s : Finset α) (a : α) :
powerset (insert a s) = s.powerset ∪ s.powerset.image (insert a) :=
by
ext t
simp only [mem_powerset, mem_image, mem_union, subset_insert_iff]
grind
