Theorems · Theorem · order theory
Finset.mul_inf_le_inf_mul_of_nonneg
∀ {ι : Type u_1} {M₀ : Type u_2} [inst : MonoidWithZero M₀] {s : Finset ι} {a b : ι → M₀} [inst_1 : SemilatticeInf M₀]
[inst_2 : OrderTop M₀] [PosMulMono M₀] [MulPosMono M₀],
(∀ i ∈ s, 0 ≤ a i) → (∀ i ∈ s, 0 ≤ b i) → s.inf a * s.inf b ≤ s.inf (a * b)- Cited by
- 0 results in Mathlib
- Foundations
- Depth 56 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
- SemilatticeInfstatement and proof · cited by 634
- OrderTopstatement and proof · cited by 493
- MonoidWithZerostatement and proof · cited by 456
- Finset.infstatement · cited by 219
- PosMulMonostatement and proof · cited by 165
- mul_le_mulproof · cited by 144
- MulPosMonostatement and proof · cited by 128
- Finset.inf_leproof · cited by 23
- Finset.le_infproof · cited by 10
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.