Prove2Me

Complement_of_Complement

Proved

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

proofwikiset-complement

The complement of the complement of a set is the set itself: (Sᶜ)ᶜ = S

Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Complement_of_Complement {α : Type _} (S : Set α) : Sᶜᶜ = S := by sorry
Source
https://proofwiki.org/wiki/Complement_of_Complement

View graph