no goals
α : Type u
β : Type v
γ : Type ?u.60890
δ : Type ?u.60893
ε : Type ?u.60896
ζ : Type ?u.60899
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
⊢ frontier (s ×ˢ t) = closure s ×ˢ frontier t ∪ frontier s ×ˢ closure t
simp only [frontier, closure_prod_eq, interior_prod_eq, prod_diff_prod]