V : Type ?u.488713
W : Type ?u.488716
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_1
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
⊢ range (NormedAddGroupHom.comp g f) = AddMonoidHom.range (AddMonoidHom.comp (toAddMonoidHom g) (toAddMonoidHom f))
V : Type ?u.488713
W : Type ?u.488716
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_1
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
⊢ range (NormedAddGroupHom.comp g f) = AddSubgroup.map (toAddMonoidHom g) (range f)
erw [AddMonoidHom.map_range]
no goals
V : Type ?u.488713
W : Type ?u.488716
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_1
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
⊢ range (NormedAddGroupHom.comp g f) = AddMonoidHom.range (AddMonoidHom.comp (toAddMonoidHom g) (toAddMonoidHom f))
rfl