no goals
α : Type u
β : Type v
γ : Type ?u.60232
δ : Type ?u.60235
ε : Type ?u.60238
ζ : Type ?u.60241
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
x✝ : α × β
a : α
b : β
⊢ (a, b) ∈ interior (s ×ˢ t) ↔ (a, b) ∈ interior s ×ˢ interior t
simp only [mem_interior_iff_mem_nhds, mem_prod, prod_mem_nhds_iff]