Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-07 09:30 322ccc54

View on Github →

feat(finset/basic): downward induction for finsets (#7379)

Estimated changes

Modified src/data/finset/basic.lean

added def finset.strong_downward_induction

added theorem finset.strong_downward_induction_eq

added def finset.strong_downward_induction_on

added theorem finset.strong_downward_induction_on_eq

Modified src/data/multiset/basic.lean

added def multiset.strong_downward_induction

added theorem multiset.strong_downward_induction_eq

added def multiset.strong_downward_induction_on

added theorem multiset.strong_downward_induction_on_eq