Commit 2024-07-12 14:35 f8516eba

View on Github →

feat: Density of a finset (#11243) The density of a finite set in an ambient group is a quantity of great interest in combinatorics. This PR defines Finset.dens s for s : Finset α as the size of s divided by the size of α, with value in any semifield. The API lemmas are copied from Finset.card (but not all Finset.card lemmas are sensible Finset.dens lemmas). From LeanAPAP

Estimated changes

modified theorem Finset.card_sdiff_add_card
added def Finset.dens
added theorem Finset.dens_cons
added theorem Finset.dens_disjUnion
added theorem Finset.dens_empty
added theorem Finset.dens_eq_one
added theorem Finset.dens_eq_zero
added theorem Finset.dens_le_dens
added theorem Finset.dens_lt_dens
added theorem Finset.dens_map_le
added theorem Finset.dens_mono
added theorem Finset.dens_ne_one
added theorem Finset.dens_ne_zero
added theorem Finset.dens_pos
added theorem Finset.dens_sdiff
added theorem Finset.dens_sdiff_comm
added theorem Finset.dens_singleton
added theorem Finset.dens_strictMono
added theorem Finset.dens_union_le
added theorem Finset.dens_univ
added theorem Finset.le_dens_sdiff