no goals
α : Type u
β : Type v
γ : Type u_3
δ : Type ?u.64152
ε : Type ?u.64155
ζ : Type ?u.64158
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
ι : Type u_1
κ : Type u_2
f : ι → β
g : κ → γ
hf : DenseRange f
hg : DenseRange g
⊢ DenseRange (Prod.map f g)
simpa only [DenseRange, prod_range_range_eq] using hf.prod hg