BigOperators

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

Statistics

Metric	Count
Definitions	0
Theorems exists_le_of_sum_le, iInf_sum, lt_top_of_sum_ne_top, prod_lt_top, prod_ne_top, sum_eq_top, sum_iSup, sum_iSup_of_monotone, sum_lt_sum_of_nonempty, sum_lt_top, sum_ne_top, toNat_prod, toNat_sum	13
Total	13

ENat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_le_of_sum_le 📖	mathematical	Finset.Nonempty ENat instLEENat Finset.sum LinearOrderedAddCommMonoidWithTop.toAddCommMonoid instLinearOrderedAddCommMonoidWithTopENat	Finset SetLike.instMembership Finset.instSetLike ENat instLEENat	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq sum_lt_sum_of_nonempty
iInf_sum 📖	mathematical	ENat instLEENat	iInf ENat ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat Finset.sum LinearOrderedAddCommMonoidWithTop.toAddCommMonoid instLinearOrderedAddCommMonoidWithTopENat	—	Finset.cons_induction_on ciInf_const Finset.sum_cons iInf_add_iInf add_le_add IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid covariant_swap_add_of_covariant_add Finset.forall_mem_cons Finset.sum_le_sum
lt_top_of_sum_ne_top 📖	mathematical	Finset SetLike.instMembership Finset.instSetLike	ENat instLTENat Top.top instTopENat	—	sum_lt_top Ne.lt_top
prod_lt_top 📖	mathematical	ENat instLTENat Top.top instTopENat	ENat instLTENat Finset.prod CommSemiring.toCommMonoid instCommSemiringENat Top.top instTopENat	—	WithTop.prod_lt_top IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd Nat.instNontrivial
prod_ne_top 📖	—	—	—	—	WithTop.prod_ne_top IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd Nat.instNontrivial
sum_eq_top 📖	mathematical	—	Finset.sum ENat LinearOrderedAddCommMonoidWithTop.toAddCommMonoid instLinearOrderedAddCommMonoidWithTopENat Top.top instTopENat Finset SetLike.instMembership Finset.instSetLike	—	WithTop.sum_eq_top
sum_iSup 📖	mathematical	ENat instLEENat	Finset.sum ENat LinearOrderedAddCommMonoidWithTop.toAddCommMonoid instLinearOrderedAddCommMonoidWithTopENat iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat	—	Finset.cons_induction iSup_zero Finset.sum_cons iSup_add_iSup add_le_add IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid covariant_swap_add_of_covariant_add Finset.sum_le_sum
sum_iSup_of_monotone 📖	mathematical	Monotone ENat instPreorderENat	Finset.sum ENat LinearOrderedAddCommMonoidWithTop.toAddCommMonoid instLinearOrderedAddCommMonoidWithTopENat iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat	—	sum_iSup exists_ge_ge
sum_lt_sum_of_nonempty 📖	mathematical	Finset.Nonempty ENat instLTENat	ENat instLTENat Finset.sum LinearOrderedAddCommMonoidWithTop.toAddCommMonoid instLinearOrderedAddCommMonoidWithTopENat	—	Finset.Nonempty.cons_induction Finset.sum_singleton Finset.mem_singleton_self Finset.sum_cons add_lt_add
sum_lt_top 📖	mathematical	—	ENat instLTENat Finset.sum LinearOrderedAddCommMonoidWithTop.toAddCommMonoid instLinearOrderedAddCommMonoidWithTopENat Top.top instTopENat	—	WithTop.sum_lt_top
sum_ne_top 📖	—	—	—	—	WithTop.sum_ne_top
toNat_prod 📖	mathematical	—	toNat Finset.prod ENat CommSemiring.toCommMonoid instCommSemiringENat Nat.instCommMonoid	—	map_prod MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass
toNat_sum 📖	mathematical	—	toNat Finset.sum ENat LinearOrderedAddCommMonoidWithTop.toAddCommMonoid instLinearOrderedAddCommMonoidWithTopENat Nat.instAddCommMonoid	—	coe_toNat sum_ne_top Nat.cast_sum Finset.sum_congr

---

← Back to Index