Theorems · Theorem · order theory
Finset.le_prod_max_one
∀ {ι : Type u_1} {s : Finset ι} {M : Type u_4} [inst : CommMonoidWithZero M] [inst_1 : LinearOrder M] [ZeroLEOneClass M]
[PosMulMono M] {i : ι}, i ∈ s → ∀ (f : ι → M), f i ≤ ∏ i ∈ s, max (f i) 1- Cited by
- 2 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- LinearOrderstatement and proof · cited by 8,572
- Finset.prodstatement and proof · cited by 2,356
- LT.lt.leproof · cited by 2,189
- CommMonoidWithZerostatement and proof · cited by 913
- LT.lt.trans_leproof · cited by 678
- zero_le_oneproof · cited by 316
- ZeroLEOneClassstatement and proof · cited by 304
- lt_or_geproof · cited by 182
- PosMulMonostatement and proof · cited by 165
- Finset.prod_le_prodproof · cited by 40
- Finset.prod_nonnegproof · cited by 39
Cited by2
Results whose statement or proof uses this declaration.
- Finset.max_abv_sum_one_leproof · cited by 1
- Finset.max_abv_sum_one_le_of_isNonarchimedeanproof · cited by 1