no goals
α : Type u
β : Type v
γ : Type u_1
δ : Type ?u.62376
ε : Type ?u.62379
ζ : Type ?u.62382
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β → γ
a : α
b : β
s : Set α
t : Set β
u : Set γ
hf : Continuous (uncurry f)
ha : a ∈ closure s
hb : b ∈ closure t
h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → f a b ∈ u
⊢ (a, b) ∈ closure (s ×ˢ t)
simpa only [closure_prod_eq] using mk_mem_prod ha hb