Union_with_Universe
Provedproofwikiset-unionuniverse
The union of a set with the universe is the universe: univ ∪ S = univ
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Union_with_Universe {α : Type _} (S : Set α) : Set.univ ∪ S = Set.univ := by sorrySource