Finset.map_add_right_Ico

theorem Finset.map_add_right_Ico : ∀ {α : Type u_2} [inst : OrderedCancelAddCommMonoid α] [inst_1 : ExistsAddOfLE α] [inst_2 : LocallyFiniteOrder α] (a b c : α), Finset.map (addRightEmbedding c) (Finset.Ico a b) = Finset.Ico (a + c) (b + c)

The theorem `Finset.map_add_right_Ico` states that for any ordered cancelable commutative monoid `α` that supports addition of elements and is a locally finite order, given three elements `a`, `b`, and `c` of `α`, the image of the interval `[a, b)` under the embedding by right-addition by `c` is the interval `[a + c, b + c)`. In other words, mapping the interval `[a, b)` in `α` via the function "add `c` to the right" results in the interval `[a + c, b + c)` in `α`.

More concisely: For any locally finite order monoid `α` with additive structure, the image of the interval `[a, b)` under right-addition by `c` is the interval `[a + c, b + c)`.