Theorems · Theorem · order theory
List.apply_prod_le_sum_map
∀ {α : Type u_5} {β : Type u_6} [inst : Monoid α] [inst_1 : AddMonoid β] [inst_2 : Preorder β] [AddLeftMono β]
(l : List α) (f : α → β), f 1 ≤ 0 → (∀ (a b : α), f (a * b) ≤ f a + f b) → f l.prod ≤ (List.map f l).sum- Cited by
- 5 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- Monoidstatement and proof · cited by 3,887
- AddMonoidstatement and proof · cited by 2,864
- le_reflproof · cited by 2,061
- AddLeftMonostatement and proof · cited by 687
- le_imp_le_of_le_of_leproof · cited by 576
- add_le_add_rightproof · cited by 37
Cited by5
Results whose statement or proof uses this declaration.
- Multiset.apply_prod_le_sum_mapproof · cited by 5
- Polynomial.natDegree_list_prod_leproof · cited by 2
- Polynomial.degree_list_prod_leproof · cited by 1
- MvPolynomial.totalDegree_list_prodproof · cited by 0
- List.sum_map_le_apply_prodproof · cited by 0