no goals
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type u_1
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
s : Set β
t : Set γ
f g : β → γ → α
h : ∀ (x : β), x ∈ s → ∀ (y : γ), y ∈ t → f x y = g x y
hf₁ : ∀ (x : β), Continuous (f x)
hf₂ : ∀ (y : γ), Continuous fun x => f x y
hg₁ : ∀ (x : β), Continuous (g x)
hg₂ : ∀ (y : γ), Continuous fun x => g x y
this : closure s ⊆ ⋂ (y : γ) (_ : y ∈ closure t), {x | f x y = g x y}
⊢ ∀ (x : β), x ∈ closure s → ∀ (y : γ), y ∈ closure t → f x y = g x y
simpa only [subset_def, mem_iInter]