Duality_Principle_for_Sets

Proved

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

dualityproofwikiset-theory

Any set-theoretic identity using intersection, union, empty set, and universal set remains valid when these are swapped with their duals.

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Data.Set.Basic

Formal statement

theorem Duality_Principle_for_Sets {α : Type _} (A B : Set α) : (A ∩ B)ᶜ = Aᶜ ∪ Bᶜ ∧ (A ∪ B)ᶜ = Aᶜ ∩ Bᶜ := by sorry

Source