BigOperators

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

Statistics

Metric	Count
Definitions	0
Theorems sum_iSup, sum_iSup_of_monotone	2
Total	2

ENat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sum_iSup 📖	mathematical	ENat Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat iSup ConditionallyCompletePartialOrderSup.toSupSet	—	Finset.cons_induction iSup_zero Finset.sum_cons iSup_add_iSup add_le_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid covariant_swap_add_of_covariant_add Finset.sum_le_sum
sum_iSup_of_monotone 📖	mathematical	Monotone ENat PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat iSup ConditionallyCompletePartialOrderSup.toSupSet	—	sum_iSup exists_ge_ge

---

← Back to Index