Sum

Statistics

Metric	Count
Definitions	0
Theorems `sum_Ico_le_sum`, `sum_le_sum_Ioc`, `sum_le_sum_range`, `sum_range_le_sum`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_Ico_le_sum` 📖	mathematical	—	`sum` `Int.instAddCommMonoid` `Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `Int.instLocallyFiniteOrder` `card`	—	`sum_inter_add_sum_diff` `le_imp_le_of_le_of_le` `le_refl` `add_le_add_right` `Int.instAddLeftMono` `sum_le_card_nsmul` `LT.lt.le` `mem_Ico` `mem_sdiff` `inter_comm` `card_sdiff_comm` `Int.card_Ico` `add_sub_cancel_left` `card_nsmul_le_sum`
`sum_le_sum_Ioc` 📖	mathematical	—	`sum` `Int.instAddCommMonoid` `Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `Int.instLocallyFiniteOrder` `card`	—	`sum_inter_add_sum_diff` `add_le_add_right` `Int.instAddLeftMono` `sum_le_card_nsmul` `mem_Ioc` `mem_sdiff` `inter_comm` `card_sdiff_comm` `Int.card_Ioc` `sub_sub_cancel` `card_nsmul_le_sum` `LT.lt.le`
`sum_le_sum_range` 📖	mathematical	—	`sum` `Int.instAddCommMonoid` `range` `card`	—	`sum_nbij` `mem_Ioc` `mem_range` `coe_range` `mem_coe` `sum_le_sum_Ioc`
`sum_range_le_sum` 📖	mathematical	—	`sum` `Int.instAddCommMonoid` `range` `card`	—	`sum_nbij` `mem_Ico` `mem_range` `coe_range` `mem_coe` `sum_Ico_le_sum`

---