List

📁 Source: Mathlib/Algebra/Order/BigOperators/Group/List.lean

Statistics

Metric	Count
Definitions	0
Theorems `prod_le_prod'`, `sum_le_sum`, `prod_le_prod'`, `sum_le_sum`, `prod_le_prod'`, `sum_le_sum`, `all_one_of_le_one_le_of_prod_eq_one`, `all_zero_of_le_zero_le_of_sum_eq_zero`, `apply_prod_le_sum_map`, `card_nsmul_le_sum`, `exists_le_of_prod_le'`, `exists_le_of_sum_le`, `exists_lt_of_prod_lt'`, `exists_lt_of_sum_lt`, `le_prod_nonempty_of_submultiplicative`, `le_prod_nonempty_of_submultiplicative_on_pred`, `le_prod_of_mem`, `le_prod_of_submultiplicative`, `le_prod_of_submultiplicative_on_pred`, `le_sum_nonempty_of_subadditive`, `le_sum_nonempty_of_subadditive_on_pred`, `le_sum_of_mem`, `le_sum_of_subadditive`, `le_sum_of_subadditive_on_pred`, `max_prod_le`, `max_sum_le`, `monotone_prod_take`, `monotone_sum_take`, `one_le_prod_of_one_le`, `one_lt_prod_of_one_lt`, `pow_card_le_prod`, `prod_eq_one_iff`, `prod_le_pow_card`, `prod_le_prod'`, `prod_lt_prod'`, `prod_lt_prod_of_ne_nil`, `prod_min_le`, `single_le_prod`, `single_le_sum`, `sum_eq_zero_iff`, `sum_le_card_nsmul`, `sum_le_foldr_max`, `sum_le_sum`, `sum_lt_sum`, `sum_lt_sum_of_ne_nil`, `sum_map_le_apply_prod`, `sum_min_le`, `sum_nonneg`, `sum_pos`	49
Total	49

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`all_one_of_le_one_le_of_prod_eq_one` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toMul`	—	—	`le_antisymm` `single_le_prod`
`all_zero_of_le_zero_le_of_sum_eq_zero` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toAdd`	—	—	`le_antisymm` `single_le_sum`
`apply_prod_le_sum_map` 📖	—	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `MulOne.toMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	—	`le_imp_le_of_le_of_le` `le_refl` `add_le_add_right`
`card_nsmul_le_sum` 📖	mathematical	`Preorder.toLE`	`AddMonoid.toNatSMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`sum_le_card_nsmul` `OrderDual.addRightMono` `OrderDual.addLeftMono`
`exists_le_of_prod_le'` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `prod_lt_prod_of_ne_nil`
`exists_le_of_sum_le` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_exists` `Mathlib.Tactic.Push.not_and_eq` `not_le` `sum_lt_sum_of_ne_nil`
`exists_lt_of_prod_lt'` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `prod_le_prod'`
`exists_lt_of_sum_lt` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_exists` `Mathlib.Tactic.Push.not_and_eq` `not_lt` `sum_le_sum`
`le_prod_nonempty_of_submultiplicative` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`MulOne.toOne`	—	`le_prod_nonempty_of_submultiplicative_on_pred`
`le_prod_nonempty_of_submultiplicative_on_pred` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`MulOne.toOne`	—	`mul_one` `prod_induction_nonempty` `le_imp_le_of_le_of_le` `le_refl` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono`
`le_prod_of_mem` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`le_mul_left`
`le_prod_of_submultiplicative` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toMul`	—	—	`le_prod_of_submultiplicative_on_pred`
`le_prod_of_submultiplicative_on_pred` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toMul`	—	—	`prod_induction` `le_imp_le_of_le_of_le` `le_refl` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono`
`le_sum_nonempty_of_subadditive` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`AddZero.toZero`	—	`le_sum_nonempty_of_subadditive_on_pred`
`le_sum_nonempty_of_subadditive_on_pred` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`AddZero.toZero`	—	`add_zero` `le_refl` `sum_induction_nonempty` `le_imp_le_of_le_of_le` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono`
`le_sum_of_mem` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`self_le_add_right` `le_add_left`
`le_sum_of_subadditive` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toAdd`	—	—	`le_sum_of_subadditive_on_pred`
`le_sum_of_subadditive_on_pred` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toAdd`	—	—	`sum_induction` `le_imp_le_of_le_of_le` `le_refl` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono`
`max_prod_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`max_le_iff` `prod_le_prod'` `le_max_left` `le_max_right`
`max_sum_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`max_le_iff` `sum_le_sum` `le_max_left` `le_max_right`
`monotone_prod_take` 📖	mathematical	—	`Monotone` `Nat.instPreorder` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`monotone_nat_of_le_succ` `lt_or_ge` `prod_take_succ` `le_self_mul` `le_trans`
`monotone_sum_take` 📖	mathematical	—	`Monotone` `Nat.instPreorder` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`monotone_nat_of_le_succ` `lt_or_ge` `sum_take_succ` `le_self_add` `le_trans` `le_refl`
`one_le_prod_of_one_le` 📖	mathematical	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`MulOne.toMul`	—	`le_refl` `one_le_mul`
`one_lt_prod_of_one_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`MulOne.toMul`	—	`mul_one` `one_lt_mul_of_lt_of_le'` `IsOrderedMonoid.toMulLeftMono` `le_of_lt`
`pow_card_le_prod` 📖	mathematical	`Preorder.toLE`	`Monoid.toNatPow` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`prod_le_pow_card` `OrderDual.mulRightMono` `OrderDual.mulLeftMono`
`prod_eq_one_iff` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toOne`	—	`all_one_of_le_one_le_of_prod_eq_one` `one_le` `prod_replicate` `one_pow`
`prod_le_pow_card` 📖	mathematical	`Preorder.toLE`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `Monoid.toNatPow`	—	`prod_replicate` `prod_le_prod'`
`prod_le_prod'` 📖	mathematical	`Preorder.toLE`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`Forall₂.prod_le_prod'`
`prod_lt_prod'` 📖	mathematical	`Preorder.toLE` `Preorder.toLT`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`mul_lt_mul_of_lt_of_le` `prod_le_prod'` `mul_lt_mul_of_le_of_lt`
`prod_lt_prod_of_ne_nil` 📖	mathematical	`Preorder.toLT`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`prod_lt_prod'` `LT.lt.le`
`prod_min_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `SemilatticeInf.toMin`	—	`le_min_iff` `prod_le_prod'` `min_le_left` `min_le_right`
`single_le_prod` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`MulOne.toMul`	—	`instIsEmptyFalse` `le_mul_of_one_le_right'` `IsOrderedMonoid.toMulLeftMono` `one_le_prod_of_one_le` `le_mul_of_one_le_of_le` `covariant_swap_mul_of_covariant_mul`
`single_le_sum` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`AddZero.toAdd`	—	`IsEmpty.forall_iff` `instIsEmptyFalse` `le_add_of_nonneg_right` `IsOrderedAddMonoid.toAddLeftMono` `sum_nonneg` `le_add_of_nonneg_of_le` `covariant_swap_add_of_covariant_add`
`sum_eq_zero_iff` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toZero`	—	`all_zero_of_le_zero_le_of_sum_eq_zero` `zero_le` `sum_replicate` `nsmul_zero`
`sum_le_card_nsmul` 📖	mathematical	`Preorder.toLE`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero` `AddMonoid.toNatSMul`	—	`sum_replicate` `sum_le_sum`
`sum_le_foldr_max` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddZero.toAdd` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	—	`LE.le.trans` `max_le_max` `le_rfl`
`sum_le_sum` 📖	mathematical	`Preorder.toLE`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`Forall₂.sum_le_sum` `forall₂_map_right_iff` `forall₂_map_left_iff` `forall₂_same`
`sum_lt_sum` 📖	mathematical	`Preorder.toLE` `Preorder.toLT`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`add_lt_add_of_lt_of_le` `sum_le_sum` `add_lt_add_of_le_of_lt`
`sum_lt_sum_of_ne_nil` 📖	mathematical	`Preorder.toLT`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`sum_lt_sum` `LT.lt.le`
`sum_map_le_apply_prod` 📖	—	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `MulOne.toMul`	—	—	`apply_prod_le_sum_map` `OrderDual.addLeftMono`
`sum_min_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero` `SemilatticeInf.toMin`	—	`le_min_iff` `sum_le_sum` `min_le_left` `min_le_right`
`sum_nonneg` 📖	mathematical	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddZero.toAdd`	—	`le_refl` `add_nonneg`
`sum_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`AddZero.toAdd`	—	`add_zero` `add_pos_of_pos_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `le_of_lt`

List.Forall₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_le_prod'` 📖	mathematical	`Preorder.toLE`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`le_refl` `mul_le_mul'`
`sum_le_sum` 📖	mathematical	`Preorder.toLE`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`le_refl` `add_le_add`

List.Sublist

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_le_prod'` 📖	mathematical	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`MulOne.toMul`	—	`le_refl` `LE.le.trans` `le_mul_of_one_le_left'` `le_imp_le_of_le_of_le` `mul_le_mul_right`
`sum_le_sum` 📖	mathematical	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddZero.toAdd`	—	`le_refl` `LE.le.trans` `le_add_of_nonneg_left` `le_imp_le_of_le_of_le` `add_le_add_right`

List.SublistForall₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_le_prod'` 📖	mathematical	`List.SublistForall₂` `Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`MulOne.toMul`	—	`List.sublistForall₂_iff` `LE.le.trans` `List.Forall₂.prod_le_prod'` `List.Sublist.prod_le_prod'`
`sum_le_sum` 📖	mathematical	`List.SublistForall₂` `Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddZero.toAdd`	—	`List.sublistForall₂_iff` `LE.le.trans` `List.Forall₂.sum_le_sum` `List.Sublist.sum_le_sum`

---

← Back to Index