Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-06 16:42 7f9dd51f

View on Github →

feat(data/finset): add strong induction rules for finset

Estimated changes

Modified data/finset.lean

added theorem finset.card_eq_succ

added theorem finset.card_le_of_subset

added theorem finset.card_lt_card

added theorem finset.case_strong_induction_on

added theorem finset.eq_of_subset_of_card_le

added theorem finset.strong_induction_on