Commit 2024-01-01 05:58 37c36be5

View on Github →

feat(Data/Finset/Card): bounds on cardinalities of explicit finsets (#9362)

Estimated changes

Modified Mathlib/Data/Finset/Card.lean

added theorem Finset.card_le_five

added theorem Finset.card_le_four

added theorem Finset.card_le_six

added theorem Finset.card_le_three

added theorem Finset.card_le_two