Algebraic properties of finset intervals

This file provides results about the interaction of algebra with Finset.Ixx.

@[simp]

theorem Finset.map_add_left_Icc {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) : map (addLeftEmbedding c) (Icc a b) = Icc (c + a) (c + b)

@[simp]

theorem Finset.map_add_right_Icc {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) : map (addRightEmbedding c) (Icc a b) = Icc (a + c) (b + c)

@[simp]

theorem Finset.map_add_left_Ico {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) : map (addLeftEmbedding c) (Ico a b) = Ico (c + a) (c + b)

@[simp]

theorem Finset.map_add_right_Ico {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) : map (addRightEmbedding c) (Ico a b) = Ico (a + c) (b + c)

@[simp]

theorem Finset.map_add_left_Ioc {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) : map (addLeftEmbedding c) (Ioc a b) = Ioc (c + a) (c + b)

@[simp]

theorem Finset.map_add_right_Ioc {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) : map (addRightEmbedding c) (Ioc a b) = Ioc (a + c) (b + c)

@[simp]

theorem Finset.map_add_left_Ioo {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) : map (addLeftEmbedding c) (Ioo a b) = Ioo (c + a) (c + b)

@[simp]

theorem Finset.map_add_right_Ioo {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) : map (addRightEmbedding c) (Ioo a b) = Ioo (a + c) (b + c)

@[simp]

theorem Finset.image_add_left_Icc {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [DecidableEq α] (a b c : α) : image (fun (x : α) => c + x) (Icc a b) = Icc (c + a) (c + b)

@[simp]

theorem Finset.image_add_left_Ico {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [DecidableEq α] (a b c : α) : image (fun (x : α) => c + x) (Ico a b) = Ico (c + a) (c + b)

@[simp]

theorem Finset.image_add_left_Ioc {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [DecidableEq α] (a b c : α) : image (fun (x : α) => c + x) (Ioc a b) = Ioc (c + a) (c + b)

@[simp]

theorem Finset.image_add_left_Ioo {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [DecidableEq α] (a b c : α) : image (fun (x : α) => c + x) (Ioo a b) = Ioo (c + a) (c + b)

@[simp]

theorem Finset.image_add_right_Icc {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [DecidableEq α] (a b c : α) : image (fun (x : α) => x + c) (Icc a b) = Icc (a + c) (b + c)

@[simp]

theorem Finset.image_add_right_Ico {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [DecidableEq α] (a b c : α) : image (fun (x : α) => x + c) (Ico a b) = Ico (a + c) (b + c)

@[simp]

theorem Finset.image_add_right_Ioc {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [DecidableEq α] (a b c : α) : image (fun (x : α) => x + c) (Ioc a b) = Ioc (a + c) (b + c)

@[simp]

theorem Finset.image_add_right_Ioo {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [DecidableEq α] (a b c : α) : image (fun (x : α) => x + c) (Ioo a b) = Ioo (a + c) (b + c)