Difference_of_Unions_is_Subset_of_Union_of_Differences
Provedproofwikiset-differenceset-theoryset-union
The difference of unions is a subset of the union of differences: (⋃ Sα) \ (⋃ Tα) ⊆ ⋃ (Sα \ Tα).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Difference_of_Unions_is_Subset_of_Union_of_Differences {α : Type _} {ι : Type _} (S T : ι → Set α) : (⋃ i, S i) \ (⋃ i, T i) ⊆ ⋃ i, (S i \ T i) := by sorrySource