ι : Type ?u.224107
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addRightEmbedding c) '' Set.Ioc a b = Set.Ioc (a + c) (b + c)
ι : Type ?u.224107
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addRightEmbedding c) (Ioc a b) = Ioc (a + c) (b + c)
rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc]
no goals
ι : Type ?u.224107
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addRightEmbedding c) '' Set.Ioc a b = Set.Ioc (a + c) (b + c)
exact Set.image_add_const_Ioc _ _ _