English
Let s and t be finite subsets of α. The power set of their union equals the join of their power sets: (s ∪ t).powerset = s.powerset ⊻ t.powerset.
Русский
Пусть s и t — конечные подмножества α. Множество подмножеств объединения равно объединению(мощностей) множеств: (s ∪ t).powerset = s.powerset ⊻ t.powerset.
LaTeX
$$$ (s \cup t).powerset = s.powerset \vee t.powerset $$$
Lean4
@[simp]
theorem powerset_union (s t : Finset α) : (s ∪ t).powerset = s.powerset ⊻ t.powerset :=
by
ext u
simp only [mem_sups, mem_powerset, sup_eq_union]
refine ⟨fun h ↦ ⟨_, inter_subset_left (s₂ := u), _, inter_subset_left (s₂ := u), ?_⟩, ?_⟩
· rwa [← union_inter_distrib_right, inter_eq_right]
· rintro ⟨v, hv, w, hw, rfl⟩
exact union_subset_union hv hw
