Big operators indexed by intervals

This file proves lemmas about ∏ x ∈ Ixx a b, f x and ∑ x ∈ Ixx a b, f x.

theorem Finset.left_mul_prod_Ioc {α : Type u_1} {β : Type u_2} [PartialOrder α] [CommMonoid β] {f : α → β} {a b : α} [LocallyFiniteOrder α] (h : a ≤ b) : f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x

theorem Finset.left_add_sum_Ioc {α : Type u_1} {β : Type u_2} [PartialOrder α] [AddCommMonoid β] {f : α → β} {a b : α} [LocallyFiniteOrder α] (h : a ≤ b) : f a + ∑ x ∈ Ioc a b, f x = ∑ x ∈ Icc a b, f x

theorem Finset.prod_Ioc_mul_left {α : Type u_1} {β : Type u_2} [PartialOrder α] [CommMonoid β] {f : α → β} {a b : α} [LocallyFiniteOrder α] (h : a ≤ b) : (∏ x ∈ Ioc a b, f x) * f a = ∏ x ∈ Icc a b, f x

theorem Finset.sum_Ioc_add_left {α : Type u_1} {β : Type u_2} [PartialOrder α] [AddCommMonoid β] {f : α → β} {a b : α} [LocallyFiniteOrder α] (h : a ≤ b) : ∑ x ∈ Ioc a b, f x + f a = ∑ x ∈ Icc a b, f x

theorem Finset.right_mul_prod_Ico {α : Type u_1} {β : Type u_2} [PartialOrder α] [CommMonoid β] {f : α → β} {a b : α} [LocallyFiniteOrder α] (h : a ≤ b) : f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x

theorem Finset.right_add_sum_Ico {α : Type u_1} {β : Type u_2} [PartialOrder α] [AddCommMonoid β] {f : α → β} {a b : α} [LocallyFiniteOrder α] (h : a ≤ b) : f b + ∑ x ∈ Ico a b, f x = ∑ x ∈ Icc a b, f x

theorem Finset.prod_Ico_mul_right {α : Type u_1} {β : Type u_2} [PartialOrder α] [CommMonoid β] {f : α → β} {a b : α} [LocallyFiniteOrder α] (h : a ≤ b) : (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Icc a b, f x

theorem Finset.sum_Ico_add_right {α : Type u_1} {β : Type u_2} [PartialOrder α] [AddCommMonoid β] {f : α → β} {a b : α} [LocallyFiniteOrder α] (h : a ≤ b) : ∑ x ∈ Ico a b, f x + f b = ∑ x ∈ Icc a b, f x

theorem Finset.left_mul_prod_Ioo {α : Type u_1} {β : Type u_2} [PartialOrder α] [CommMonoid β] {f : α → β} {a b : α} [LocallyFiniteOrder α] (h : a < b) : f a * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ico a b, f x

theorem Finset.left_add_sum_Ioo {α : Type u_1} {β : Type u_2} [PartialOrder α] [AddCommMonoid β] {f : α → β} {a b : α} [LocallyFiniteOrder α] (h : a < b) : f a + ∑ x ∈ Ioo a b, f x = ∑ x ∈ Ico a b, f x

theorem Finset.prod_Ioo_mul_left {α : Type u_1} {β : Type u_2} [PartialOrder α] [CommMonoid β] {f : α → β} {a b : α} [LocallyFiniteOrder α] (h : a < b) : (∏ x ∈ Ioo a b, f x) * f a = ∏ x ∈ Ico a b, f x

theorem Finset.sum_Ioo_add_left {α : Type u_1} {β : Type u_2} [PartialOrder α] [AddCommMonoid β] {f : α → β} {a b : α} [LocallyFiniteOrder α] (h : a < b) : ∑ x ∈ Ioo a b, f x + f a = ∑ x ∈ Ico a b, f x

theorem Finset.right_mul_prod_Ioo {α : Type u_1} {β : Type u_2} [PartialOrder α] [CommMonoid β] {f : α → β} {a b : α} [LocallyFiniteOrder α] (h : a < b) : f b * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ioc a b, f x

theorem Finset.right_add_sum_Ioo {α : Type u_1} {β : Type u_2} [PartialOrder α] [AddCommMonoid β] {f : α → β} {a b : α} [LocallyFiniteOrder α] (h : a < b) : f b + ∑ x ∈ Ioo a b, f x = ∑ x ∈ Ioc a b, f x

theorem Finset.prod_Ioo_mul_right {α : Type u_1} {β : Type u_2} [PartialOrder α] [CommMonoid β] {f : α → β} {a b : α} [LocallyFiniteOrder α] (h : a < b) : (∏ x ∈ Ioo a b, f x) * f b = ∏ x ∈ Ioc a b, f x

theorem Finset.sum_Ioo_add_right {α : Type u_1} {β : Type u_2} [PartialOrder α] [AddCommMonoid β] {f : α → β} {a b : α} [LocallyFiniteOrder α] (h : a < b) : ∑ x ∈ Ioo a b, f x + f b = ∑ x ∈ Ioc a b, f x

theorem Finset.left_mul_prod_Ioi {α : Type u_1} {β : Type u_2} [PartialOrder α] [CommMonoid β] {f : α → β} [LocallyFiniteOrderTop α] (a : α) : f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ Ici a, f x

theorem Finset.left_add_sum_Ioi {α : Type u_1} {β : Type u_2} [PartialOrder α] [AddCommMonoid β] {f : α → β} [LocallyFiniteOrderTop α] (a : α) : f a + ∑ x ∈ Ioi a, f x = ∑ x ∈ Ici a, f x

theorem Finset.prod_Ioi_mul_left {α : Type u_1} {β : Type u_2} [PartialOrder α] [CommMonoid β] {f : α → β} [LocallyFiniteOrderTop α] (a : α) : (∏ x ∈ Ioi a, f x) * f a = ∏ x ∈ Ici a, f x

theorem Finset.sum_Ioi_add_left {α : Type u_1} {β : Type u_2} [PartialOrder α] [AddCommMonoid β] {f : α → β} [LocallyFiniteOrderTop α] (a : α) : ∑ x ∈ Ioi a, f x + f a = ∑ x ∈ Ici a, f x

theorem Finset.right_mul_prod_Iio {α : Type u_1} {β : Type u_2} [PartialOrder α] [CommMonoid β] {f : α → β} [LocallyFiniteOrderBot α] (a : α) : f a * ∏ x ∈ Iio a, f x = ∏ x ∈ Iic a, f x

theorem Finset.right_add_sum_Iio {α : Type u_1} {β : Type u_2} [PartialOrder α] [AddCommMonoid β] {f : α → β} [LocallyFiniteOrderBot α] (a : α) : f a + ∑ x ∈ Iio a, f x = ∑ x ∈ Iic a, f x

theorem Finset.prod_Iio_mul_right {α : Type u_1} {β : Type u_2} [PartialOrder α] [CommMonoid β] {f : α → β} [LocallyFiniteOrderBot α] (a : α) : (∏ x ∈ Iio a, f x) * f a = ∏ x ∈ Iic a, f x

theorem Finset.sum_Iio_add_right {α : Type u_1} {β : Type u_2} [PartialOrder α] [AddCommMonoid β] {f : α → β} [LocallyFiniteOrderBot α] (a : α) : ∑ x ∈ Iio a, f x + f a = ∑ x ∈ Iic a, f x