no goals
α : Type u
β : Type v
γ : Type ?u.61421
δ : Type ?u.61424
ε : Type ?u.61427
ζ : Type ?u.61430
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
⊢ frontier (s ×ˢ univ) = frontier s ×ˢ univ
simp [frontier_prod_eq]