feat(data/set/finite): add lemma about to_finset of complement of set (#5881)
feat(data/set/finite): add lemma about to_finset of complement of set (#5881)

Add lemma stating that taking to_finset of the complement of a set is the same thing as taking the complement of to_finset of the set.



Co-authored-by: agusakov <067de2d7f4f5809454de1022e9c3aab9efe72888@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib