English
The powerset of s with a inserted equals the union of the powerset of s and the image of the powerset under insertion of a: 𝒫(s ∪ {a}) = 𝒫(s) ∪ {a}'' 𝒫(s).
Русский
Мощности множества s ∪ {a} равны объединению мощностей s и образа мощностей s при добавлении a: 𝒫(s ∪ {a}) = 𝒫(s) ∪ {a}'' 𝒫(s).
LaTeX
$$$\\mathcal{P}(insert\\ a\\ s) = \\mathcal{P}(s) \\cup insert\\ a''\\mathcal{P}(s)$$$
Lean4
/-- The powerset of `{a} ∪ s` is `𝒫 s` together with `{a} ∪ t` for each `t ∈ 𝒫 s`. -/
theorem powerset_insert (s : Set α) (a : α) : 𝒫 insert a s = 𝒫 s ∪ insert a '' 𝒫 s :=
by
ext t
constructor
· intro h
by_cases hs : a ∈ t
· right
refine ⟨t \ { a }, by grind⟩
· grind
· grind
