ι : Type ?u.210544
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addLeftEmbedding c) '' Set.Icc a b = Set.Icc (c + a) (c + b)
ι : Type ?u.210544
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addLeftEmbedding c) (Icc a b) = Icc (c + a) (c + b)
rw [← coe_inj, coe_map, coe_Icc, coe_Icc]
no goals
ι : Type ?u.210544
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addLeftEmbedding c) '' Set.Icc a b = Set.Icc (c + a) (c + b)
exact Set.image_const_add_Icc _ _ _