Auxiliary Finset lemmas

Small helper lemmas about Finset that are not specific to Boolean functions.

@[simp]

theorem Finset.filter_univ_not_mem {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : {x : α | x ∉ s} = sᶜ