Theorems · Theorem · order theory
Finset.prod_lt_prod_of_nonempty
∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R]
[PosMulStrictMono R] [Nontrivial R] {f g : ι → R} {s : Finset ι},
(∀ i ∈ s, 0 < f i) → (∀ i ∈ s, f i < g i) → s.Nonempty → ∏ i ∈ s, f i < ∏ i ∈ s, g i- Cited by
- 2 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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
- PartialOrderstatement and proof · cited by 6,410
- Nontrivialstatement and proof · cited by 2,416
- Finset.prodstatement · cited by 2,356
- le_of_ltproof · cited by 1,175
- Finset.Nonemptystatement and proof · cited by 1,001
- CommMonoidWithZerostatement and proof · cited by 913
- ZeroLEOneClassstatement and proof · cited by 304
- PosMulStrictMonostatement and proof · cited by 151
- Finset.prod_lt_prodproof · cited by 1
Cited by2
Results whose statement or proof uses this declaration.
- NumberField.InfinitePlace.one_le_of_lt_oneproof · cited by 2
- BoundingSieve.nu_lt_one_of_dvd_prodPrimesproof · cited by 0