Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-23 14:34 6537ae9c

View on Github →

feat(order/partition/finpartition): Bound size of a bit of finpartition.atomise (#15350) Auxiliary lemmas for Szemerédi Regularity Lemma.

Estimated changes

Modified src/order/partition/finpartition.lean

modified theorem finpartition.bUnion_filter_atomise

added theorem finpartition.card_filter_atomise_le_two_pow

modified theorem finpartition.mem_atomise