mathlib

66cc2980 - feat(data/finset): existence of a smaller set (#2420)

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.