Theorems · Theorem · order theory
WithTop.prod_lt_top
∀ {ι : Type u_1} {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [inst_1 : NoZeroDivisors M₀] [inst_2 : Nontrivial M₀]
[inst_3 : DecidableEq M₀] {s : Finset ι} {f : ι → WithTop M₀} [inst_4 : LT M₀], (∀ i ∈ s, f i < ⊤) → ∏ i ∈ s, f i < ⊤A product of finite terms is finite.
- Defined in
- Mathlib.Algebra.BigOperators.WithTop
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 55 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
- Top.topstatement and proof · cited by 9,680
- WithTopstatement and proof · cited by 3,754
- Nontrivialstatement and proof · cited by 2,416
- Finset.prodstatement · cited by 2,356
- CommMonoidWithZerostatement and proof · cited by 913
- NoZeroDivisorsstatement and proof · cited by 545
- WithTop.coe_lt_topproof · cited by 44
- Finset.prod_inductionproof · cited by 18
- WithTop.mul_lt_topproof · cited by 4
Cited by2
Results whose statement or proof uses this declaration.
- ENNReal.prod_lt_topproof · cited by 0
- ENat.prod_lt_topproof · cited by 0