theorem Set.eq_empty_of_forall_notMem
theorem Set.eq_empty_of_forall_notMem: ∀ {α : Type u} {s : Set α}, (∀ (x : α), ¬x ∈ s) → s = ∅
theorem Set.eq_empty_of_forall_notMem
theorem Set.eq_empty_of_forall_notMem: ∀ {α : Type u} {s : Set α}, (∀ (x : α), ¬x ∈ s) → s = ∅