Documentation Verification Report

Sum

📁 Source: Mathlib/Data/Multiset/Sum.lean

Statistics

Metric	Count
Definitions `disjSum`	1
Theorems `disjSum`, `card_disjSum`, `disjSum_lt_disjSum_of_le_of_lt`, `disjSum_lt_disjSum_of_lt_of_le`, `disjSum_mono`, `disjSum_mono_left`, `disjSum_mono_right`, `disjSum_strictMono_left`, `disjSum_strictMono_right`, `disjSum_zero`, `inl_mem_disjSum`, `inr_mem_disjSum`, `map_disjSum`, `mem_disjSum`, `zero_disjSum`	15
Total	16

Multiset

Definitions

Name	Category	Theorems
`disjSum` 📖	CompOp	16 math math: `Finset.val_disjSum`, `inr_mem_disjSum`, `disjSum_lt_disjSum_of_le_of_lt`, `disjSum_strictMono_left`, `inl_mem_disjSum`, `disjSum_lt_disjSum_of_lt_of_le`, `mem_disjSum`, `disjSum_zero`, `disjSum_mono_right`, `disjSum_mono`, `map_disjSum`, `card_disjSum`, `disjSum_strictMono_right`, `Nodup.disjSum`, `zero_disjSum`, `disjSum_mono_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_disjSum` 📖	mathematical	—	`card` `disjSum`	—	`disjSum.eq_1` `card_add` `card_map`
`disjSum_lt_disjSum_of_le_of_lt` 📖	mathematical	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Preorder.toLT`	`disjSum`	—	`add_lt_add_of_le_of_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `instAddLeftMono` `covariant_swap_add_of_covariant_add` `map_le_map` `map_lt_map`
`disjSum_lt_disjSum_of_lt_of_le` 📖	mathematical	`Multiset` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Preorder.toLE`	`disjSum`	—	`add_lt_add_of_lt_of_le` `instAddLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `map_lt_map` `map_le_map`
`disjSum_mono` 📖	mathematical	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`disjSum`	—	`add_le_add` `instAddLeftMono` `covariant_swap_add_of_covariant_add` `map_le_map`
`disjSum_mono_left` 📖	mathematical	—	`Monotone` `Multiset` `PartialOrder.toPreorder` `instPartialOrder` `disjSum`	—	`add_le_add_right` `map_le_map`
`disjSum_mono_right` 📖	mathematical	—	`Monotone` `Multiset` `PartialOrder.toPreorder` `instPartialOrder` `disjSum`	—	`add_le_add_left` `map_le_map`
`disjSum_strictMono_left` 📖	mathematical	—	`StrictMono` `Multiset` `PartialOrder.toPreorder` `instPartialOrder` `disjSum`	—	`disjSum_lt_disjSum_of_lt_of_le` `le_rfl`
`disjSum_strictMono_right` 📖	mathematical	—	`StrictMono` `Multiset` `PartialOrder.toPreorder` `instPartialOrder` `disjSum`	—	`disjSum_lt_disjSum_of_le_of_lt` `le_rfl`
`disjSum_zero` 📖	mathematical	—	`disjSum` `Multiset` `instZero` `map`	—	`add_zero`
`inl_mem_disjSum` 📖	mathematical	—	`Multiset` `instMembership` `disjSum`	—	`mem_disjSum`
`inr_mem_disjSum` 📖	mathematical	—	`Multiset` `instMembership` `disjSum`	—	`mem_disjSum`
`map_disjSum` 📖	mathematical	—	`map` `disjSum` `Multiset` `instAdd`	—	`map_add` `map_map` `map_congr`
`mem_disjSum` 📖	mathematical	—	`Multiset` `instMembership` `disjSum`	—	—
`zero_disjSum` 📖	mathematical	—	`disjSum` `Multiset` `instZero` `map`	—	`zero_add`

Multiset.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjSum` 📖	mathematical	`Multiset.Nodup`	`Multiset.disjSum`	—	`add_iff` `map` `Sum.inl_injective` `Sum.inr_injective` `Multiset.disjoint_map_map`

---

← Back to Index