Algebraic properties of multiset intervals

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

theorem Multiset.map_add_left_Icc {α : Type u_1} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Multiset.map (fun (x : α) => c + x) (Multiset.Icc a b) = Multiset.Icc (c + a) (c + b)

theorem Multiset.map_add_left_Ico {α : Type u_1} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Multiset.map (fun (x : α) => c + x) (Multiset.Ico a b) = Multiset.Ico (c + a) (c + b)

theorem Multiset.map_add_left_Ioc {α : Type u_1} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Multiset.map (fun (x : α) => c + x) (Multiset.Ioc a b) = Multiset.Ioc (c + a) (c + b)

theorem Multiset.map_add_left_Ioo {α : Type u_1} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Multiset.map (fun (x : α) => c + x) (Multiset.Ioo a b) = Multiset.Ioo (c + a) (c + b)

theorem Multiset.map_add_right_Icc {α : Type u_1} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Multiset.map (fun (x : α) => x + c) (Multiset.Icc a b) = Multiset.Icc (a + c) (b + c)

theorem Multiset.map_add_right_Ico {α : Type u_1} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Multiset.map (fun (x : α) => x + c) (Multiset.Ico a b) = Multiset.Ico (a + c) (b + c)

theorem Multiset.map_add_right_Ioc {α : Type u_1} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Multiset.map (fun (x : α) => x + c) (Multiset.Ioc a b) = Multiset.Ioc (a + c) (b + c)

theorem Multiset.map_add_right_Ioo {α : Type u_1} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Multiset.map (fun (x : α) => x + c) (Multiset.Ioo a b) = Multiset.Ioo (a + c) (b + c)