Intersection_with_Universe
Provedproofwikiset-intersectionuniverse
The intersection of a set with the universe is the set itself: univ ∩ S = S
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Intersection_with_Universe {α : Type _} (S : Set α) : Set.univ ∩ S = S := by sorrySource