no goals
α : Type u
β : Type v
ι : Type ?u.103613
π : ι → Type ?u.103618
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ NoncompactSpace (α × β) ↔ NoncompactSpace α ∧ Nonempty β ∨ Nonempty α ∧ NoncompactSpace β
simp [← Filter.cocompact_neBot_iff, ← Filter.coprod_cocompact, Filter.coprod_neBot_iff]