Commit 2026-10-17 12:44 1e2bb27d

View on Github →

feat: Finset.exists_mem_cons (#44919) We already have Finset.exists_mem_insert and Finset.forall_mem_cons, so add a lemma Finset.exists_mem_cons as well.

Estimated changes

added theorem Finset.exists_mem_cons