Union_of_Power_Sets
Provedpower-setproofwikiset-unionsubsets
The union of the power sets of two sets S and T is a subset of the power set of their union: 𝒫(S) ∪ 𝒫(T) ⊆ 𝒫(S ∪ T).
Preamble
import Mathlib.Data.Set.Lattice
Formal statement
theorem Union_of_Power_Sets {α : Type _} (S T : Set α) : Set.powerset S ∪ Set.powerset T ⊆ Set.powerset (S ∪ T) := by sorrySource