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