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