PiInduction

Statistics

Metric	Count
Definitions	0
Theorems `induction_on_pi`, `induction_on_pi_max`, `induction_on_pi_min`, `induction_on_pi_of_choice`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`induction_on_pi` 📖	—	`Finset` `instEmptyCollection` `Function.update` `instInsert`	—	—	`induction_on_pi_of_choice` `notMem_erase`
`induction_on_pi_max` 📖	—	`Finset` `instEmptyCollection` `Function.update` `instInsert`	—	—	`induction_on_pi_of_choice` `max'_mem` `lt_max'_of_mem_erase_max'`
`induction_on_pi_min` 📖	—	`Finset` `instEmptyCollection` `Function.update` `instInsert`	—	—	`induction_on_pi_max`
`induction_on_pi_of_choice` 📖	—	`Finset` `instMembership` `erase` `instEmptyCollection` `Function.update` `instInsert`	—	—	`nonempty_fintype` `eq_empty_or_nonempty` `sigma_nonempty` `Function.update_self` `notMem_erase` `Function.update_idem` `insert_erase` `Function.update_eq_self` `erase_insert` `ssubset_iff_of_subset` `sigma_mono` `Subset.refl` `le_update_iff` `subset_insert` `le_rfl` `mem_sigma` `mem_univ`

---