Results about big operators over intervals #
We prove results about big operators over intervals.
theorem
Finset.prod_Ico_add'
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedCancelAddMonoid α]
[ExistsAddOfLE α]
[LocallyFiniteOrder α]
(f : α → M)
(a b c : α)
:
theorem
Finset.sum_Ico_add'
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedCancelAddMonoid α]
[ExistsAddOfLE α]
[LocallyFiniteOrder α]
(f : α → M)
(a b c : α)
:
theorem
Finset.prod_Ico_add
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedCancelAddMonoid α]
[ExistsAddOfLE α]
[LocallyFiniteOrder α]
(f : α → M)
(a b c : α)
:
theorem
Finset.sum_Ico_add
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedCancelAddMonoid α]
[ExistsAddOfLE α]
[LocallyFiniteOrder α]
(f : α → M)
(a b c : α)
:
@[simp]
theorem
Finset.prod_Ico_add_right_sub_eq
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
{f : α → M}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedCancelAddMonoid α]
[ExistsAddOfLE α]
[LocallyFiniteOrder α]
[Sub α]
[OrderedSub α]
(a b c : α)
:
@[simp]
theorem
Finset.sum_Ico_add_right_sub_eq
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
{f : α → M}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedCancelAddMonoid α]
[ExistsAddOfLE α]
[LocallyFiniteOrder α]
[Sub α]
[OrderedSub α]
(a b c : α)
: