ι : Type ?u.242100
α : Type u_1
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Ioo a b) = image (↑(addLeftEmbedding c)) (Ioo a b)
ι : Type ?u.242100
α : Type u_1
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Ioo a b) = Ioo (c + a) (c + b)
rw [← map_add_left_Ioo, map_eq_image]
no goals
ι : Type ?u.242100
α : Type u_1
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Ioo a b) = image (↑(addLeftEmbedding c)) (Ioo a b)
rfl