Bounds

Statistics

Metric	Count
Definitions	0
Theorems `range_comp_of_nonneg`, `bddAbove_range_mul`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`range_comp_of_nonneg` 📖	—	`BddAbove` `Preorder.toLE` `Set.range` `Pi.hasLe` `Pi.instZero` `MonotoneOn` `setOf`	—	—	`MonotoneOn.map_bddAbove` `le_trans` `Set.range_comp`

Name	Kind	Assumes	Proves	Validates	Depends On
`bddAbove_range_mul` 📖	mathematical	`BddAbove` `Preorder.toLE` `Set.range` `Pi.hasLe` `Pi.instZero`	`Pi.instMul`	—	`BddAbove.range_comp_of_nonneg` `bddAbove_range_prod` `MonotoneOn.mul` `Monotone.monotoneOn` `monotone_fst` `monotone_snd`

---