α : Type ?u.176030
β : Type u_2
γ : Type u_1
δ : Type ?u.176039
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
κ : Type u_3
ι : Type ?u.176054
f✝ : κ → β
g✝ g : β → γ
f : κ → β
hg : DenseRange g
hf : DenseRange f
cg : Continuous g
⊢ Dense (g '' range f)
α : Type ?u.176030
β : Type u_2
γ : Type u_1
δ : Type ?u.176039
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
κ : Type u_3
ι : Type ?u.176054
f✝ : κ → β
g✝ g : β → γ
f : κ → β
hg : DenseRange g
hf : DenseRange f
cg : Continuous g
⊢ DenseRange (g ∘ f)
rw [DenseRange, range_comp]
no goals
α : Type ?u.176030
β : Type u_2
γ : Type u_1
δ : Type ?u.176039
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
κ : Type u_3
ι : Type ?u.176054
f✝ : κ → β
g✝ g : β → γ
f : κ → β
hg : DenseRange g
hf : DenseRange f
cg : Continuous g
⊢ Dense (g '' range f)
exact hg.dense_image cg hf