Commit 2020-04-15 22:29 66cc2980
View on Github →feat(data/finset): existence of a smaller set (#2420) Show the existence of a smaller finset contained in a given finset. The next in my series of lemmas for my combinatorics project.
feat(data/finset): existence of a smaller set (#2420) Show the existence of a smaller finset contained in a given finset. The next in my series of lemmas for my combinatorics project.