no goals
α : Type u
β : Type v
γ : Type ?u.63391
δ : Type ?u.63394
ε : Type ?u.63397
ζ : Type ?u.63400
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s₁ : Set α
s₂ : Set β
h₁ : IsClosed s₁
h₂ : IsClosed s₂
⊢ closure (s₁ ×ˢ s₂) = s₁ ×ˢ s₂
simp only [h₁.closure_eq, h₂.closure_eq, closure_prod_eq]