Commit 2023-11-14 13:27 1e1b274e

View on Github →

feat: Finset of arbitrary size in an infinite type (#8348) and a few other easy lemmas

Estimated changes

Modified Mathlib/Data/Set/Finite.lean

added theorem Finset.exists_card_eq

added theorem Finset.exists_not_mem

added theorem Set.Finite.exists_not_mem

added theorem Set.Finite.of_surjOn

added theorem Set.Infinite.exists_not_mem_finite

modified theorem Set.Infinite.exists_not_mem_finset