Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-26 19:37 080362d0

View on Github →

feat(data/finset/pi_induction): induction on Π i, finset (α i) (#8794)

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.not_ssubset_empty

added theorem finset.sigma_eq_empty

modified theorem finset.sigma_mono

added theorem finset.sigma_nonempty

modified def option.to_finset

Created src/data/finset/pi_induction.lean

added theorem finset.induction_on_pi

added theorem finset.induction_on_pi_max

added theorem finset.induction_on_pi_min

added theorem finset.induction_on_pi_of_choice