Documentation

LeanPool.LeanBooleanfun.ToMathlib.Finset

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 : α | xs} = s