Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-25 17:49 ba876475

View on Github →

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.

Estimated changes