Union_of_Intersections

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

proofwikiset-intersectionset-theoryset-union

(S1 ∩ S2) ∪ (T1 ∩ T2) ⊆ S1 ∪ T1.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Union_of_Intersections {α : Type _} (S₁ S₂ T₁ T₂ : Set α) : (S₁ ∩ S₂) ∪ (T₁ ∩ T₂) ⊆ S₁ ∪ T₁ := by sorry

Source