Union_with_Empty_Set

Proved

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

empty-setproofwikiset-unionsubsetsunion-with-empty-set

The union of any set with the empty set is the set itself $S \cup \O = S$

Preamble

import Mathlib.Data.Set.Basic

Formal statement

theorem Union_with_Empty_Set {α : Type*} (S : Set α) : S ∪ ∅ = S := by sorry

Source