Documentation Verification Report

SubsetSum

📁 Source: Mathlib/Combinatorics/Additive/SubsetSum.lean

Statistics

Metric	Count
Definitions `subsetSum`	1
Theorems `card_add_card_subsetSum_lt_card_subsetSum_insert_max`, `card_choose_two_lt_card_subsetSum_of_nonneg`, `card_succ_choose_two_lt_card_subsetSum_of_pos`, `mem_subsetSum_iff`, `nonneg_of_mem_subsetSum`, `subsetSum_erase_zero`, `subsetSum_mono`, `subsetSum_nonempty`, `subset_subsetSum`, `vadd_finset_subsetSum_subset_subsetSum_insert`, `zero_mem_subsetSum`	11
Total	12

Finset

Definitions

Name	Category	Theorems
`subsetSum` 📖	CompOp	10 math math: `card_choose_two_lt_card_subsetSum_of_nonneg`, `zero_mem_subsetSum`, `mem_subsetSum_iff`, `card_add_card_subsetSum_lt_card_subsetSum_insert_max`, `subsetSum_erase_zero`, `card_succ_choose_two_lt_card_subsetSum_of_pos`, `vadd_finset_subsetSum_subset_subsetSum_insert`, `subsetSum_nonempty`, `subset_subsetSum`, `subsetSum_mono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_add_card_subsetSum_lt_card_subsetSum_insert_max` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`card` `subsetSum` `Finset` `instInsert`	—	`nonneg_of_mem_subsetSum` `LT.lt.le` `LT.lt.ne'` `add_pos_of_pos_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `lt_add_of_lt_of_nonneg` `insert_subset_iff` `mem_of_subset` `subsetSum_mono` `subset_insert` `Mathlib.Tactic.GCongr.rel_imp_rel` `instIsTransSubset` `subset_refl` `instReflSubset` `zero_mem_subsetSum` `subset_subsetSum` `vadd_finset_subsetSum_subset_subsetSum_insert` `LT.lt.false` `add_lt_add_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `Nat.instIsOrderedAddMonoid` `card_insert_of_notMem` `card_image_of_injOn` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `card_union_of_disjoint` `le_imp_le_of_le_of_le` `card_le_card` `union_subset` `le_refl`
`card_choose_two_lt_card_subsetSum_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Nat.choose` `card` `subsetSum`	—	`le_imp_le_of_le_of_le` `Nat.choose_le_choose` `tsub_le_iff_right` `Nat.instOrderedSub` `pred_card_le_card_erase` `le_refl` `card_succ_choose_two_lt_card_subsetSum_of_pos` `LE.le.lt_of_ne` `mem_of_mem_erase` `ne_of_mem_erase` `subsetSum_erase_zero`
`card_succ_choose_two_lt_card_subsetSum_of_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Nat.choose` `card` `subsetSum`	—	`induction_on_max` `zero_add` `Nat.choose_succ_self` `mem_insert_of_mem` `card_insert_of_notMem` `LT.lt.false` `Nat.choose_succ_left` `Nat.choose_one_right` `add_right_comm` `add_assoc` `lt_imp_lt_of_le_of_le` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `le_refl` `card_add_card_subsetSum_lt_card_subsetSum_insert_max` `mem_insert_self`
`mem_subsetSum_iff` 📖	mathematical	—	`Finset` `instMembership` `subsetSum` `instHasSubset` `sum`	—	`sum_congr`
`nonneg_of_mem_subsetSum` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset` `instMembership` `subsetSum`	—	—	`sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid`
`subsetSum_erase_zero` 📖	mathematical	—	`subsetSum` `erase` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`le_antisymm` `subsetSum_mono` `erase_subset` `mem_subsetSum_iff` `mem_erase` `mem_of_mem_erase` `sum_erase`
`subsetSum_mono` 📖	mathematical	`Finset` `instHasSubset`	`subsetSum`	—	`image_mono` `powerset_mono`
`subsetSum_nonempty` 📖	mathematical	—	`Nonempty` `subsetSum`	—	—
`subset_subsetSum` 📖	mathematical	—	`Finset` `instHasSubset` `subsetSum`	—	`mem_subsetSum_iff` `sum_singleton`
`vadd_finset_subsetSum_subset_subsetSum_insert` 📖	mathematical	`Finset` `instMembership`	`instHasSubset` `HVAdd.hVAdd` `instHVAdd` `vaddFinset` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `subsetSum` `instInsert`	—	`sum_insert`
`zero_mem_subsetSum` 📖	mathematical	—	`Finset` `instMembership` `subsetSum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`mem_subsetSum_iff` `empty_subset` `sum_empty`

---

← Back to Index