BigOperators

📁 Source: Mathlib/Data/ENNReal/BigOperators.lean

Statistics

Metric	Count
Definitions	0
Theorems `coe_finset_prod`, `coe_finset_sum`, `exists_le_of_sum_le`, `finsetSum_iSup`, `finsetSum_iSup_of_monotone`, `iInf_sum`, `lt_top_of_sum_ne_top`, `ofReal_prod_of_nonneg`, `ofReal_sum_of_nonneg`, `prod_div_distrib`, `prod_div_distrib_of_ne_top`, `prod_div_distrib_of_ne_zero`, `prod_inv_distrib`, `prod_lt_top`, `prod_ne_top`, `sum_eq_top`, `sum_lt_sum_of_nonempty`, `sum_lt_top`, `sum_ne_top`, `toNNReal_prod`, `toNNReal_sum`, `toReal_prod`, `toReal_sum`	23
Total	23

ENNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_finset_prod` 📖	mathematical	—	`ofNNReal` `Finset.prod` `NNReal` `CommSemiring.toCommMonoid` `instCommSemiringNNReal` `ENNReal` `instCommSemiring`	—	`map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`coe_finset_sum` 📖	mathematical	—	`ofNNReal` `Finset.sum` `NNReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `ENNReal` `instAddCommMonoid`	—	`map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`exists_le_of_sum_le` 📖	mathematical	`Finset.Nonempty` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Finset.sum` `instAddCommMonoid`	`Finset` `Finset.instMembership`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `sum_lt_sum_of_nonempty`
`finsetSum_iSup` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Finset.sum` `instAddCommMonoid` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder`	—	`Finset.cons_induction` `iSup_zero` `Finset.sum_cons` `iSup_add_iSup` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Finset.sum_le_sum`
`finsetSum_iSup_of_monotone` 📖	mathematical	`Monotone` `ENNReal` `PartialOrder.toPreorder` `instPartialOrder`	`Finset.sum` `instAddCommMonoid` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder`	—	`finsetSum_iSup` `exists_ge_ge`
`iInf_sum` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder` `Finset.sum` `instAddCommMonoid`	—	`Finset.cons_induction_on` `ciInf_const` `Finset.sum_cons` `iInf_add_iInf` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Finset.forall_mem_cons` `Finset.sum_le_sum`
`lt_top_of_sum_ne_top` 📖	mathematical	`Finset` `Finset.instMembership`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Top.top` `instTopENNReal`	—	`sum_lt_top` `Ne.lt_top`
`ofReal_prod_of_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`ofReal` `Finset.prod` `Real.instCommMonoid` `ENNReal` `CommSemiring.toCommMonoid` `instCommSemiring`	—	`Finset.prod_congr` `Real.toNNReal_prod_of_nonneg`
`ofReal_sum_of_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`ofReal` `Finset.sum` `Real.instAddCommMonoid` `ENNReal` `instAddCommMonoid`	—	`Finset.sum_congr` `Real.toNNReal_sum_of_nonneg`
`prod_div_distrib` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `ENNReal` `instZeroENNReal` `Top.top` `instTopENNReal`	`Finset.prod` `CommSemiring.toCommMonoid` `instCommSemiring` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`Finset.prod_congr` `div_eq_mul_inv` `prod_inv_distrib`
`prod_div_distrib_of_ne_top` 📖	mathematical	—	`Finset.prod` `ENNReal` `CommSemiring.toCommMonoid` `instCommSemiring` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`prod_div_distrib`
`prod_div_distrib_of_ne_zero` 📖	mathematical	—	`Finset.prod` `ENNReal` `CommSemiring.toCommMonoid` `instCommSemiring` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`prod_div_distrib`
`prod_inv_distrib` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `ENNReal` `instZeroENNReal` `Top.top` `instTopENNReal`	`instInv` `Finset.prod` `CommSemiring.toCommMonoid` `instCommSemiring`	—	`Finset.cons_induction` `inv_one` `Finset.prod_cons` `Set.Pairwise.mono` `Finset.coe_cons` `mul_inv` `not_or_of_imp` `prod_ne_top` `imp_iff_not_or` `Finset.prod_ne_zero_iff` `instNoZeroDivisors`
`prod_lt_top` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Top.top` `instTopENNReal`	`Finset.prod` `CommSemiring.toCommMonoid` `instCommSemiring`	—	`WithTop.prod_lt_top` `NNReal.instNoZeroDivisors`
`prod_ne_top` 📖	—	—	—	—	`WithTop.prod_ne_top` `NNReal.instNoZeroDivisors`
`sum_eq_top` 📖	mathematical	—	`Finset.sum` `ENNReal` `instAddCommMonoid` `Top.top` `instTopENNReal` `Finset` `Finset.instMembership`	—	`WithTop.sum_eq_top`
`sum_lt_sum_of_nonempty` 📖	mathematical	`Finset.Nonempty` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder`	`Finset.sum` `instAddCommMonoid`	—	`Finset.Nonempty.cons_induction` `Finset.sum_singleton` `Finset.mem_singleton_self` `Finset.sum_cons` `add_lt_add`
`sum_lt_top` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Finset.sum` `instAddCommMonoid` `Top.top` `instTopENNReal`	—	`WithTop.sum_lt_top`
`sum_ne_top` 📖	—	—	—	—	`WithTop.sum_ne_top`
`toNNReal_prod` 📖	mathematical	—	`toNNReal` `Finset.prod` `ENNReal` `CommSemiring.toCommMonoid` `instCommSemiring` `NNReal` `instCommSemiringNNReal`	—	`map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`toNNReal_sum` 📖	mathematical	—	`toNNReal` `Finset.sum` `ENNReal` `instAddCommMonoid` `NNReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`coe_toNNReal` `sum_ne_top` `coe_finset_sum` `Finset.sum_congr`
`toReal_prod` 📖	mathematical	—	`toReal` `Finset.prod` `ENNReal` `CommSemiring.toCommMonoid` `instCommSemiring` `Real` `Real.instCommMonoid`	—	`map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`toReal_sum` 📖	mathematical	—	`toReal` `Finset.sum` `ENNReal` `instAddCommMonoid` `Real` `Real.instAddCommMonoid`	—	`toReal.eq_1` `toNNReal_sum` `NNReal.coe_sum`

---

← Back to Index