no goals
α : Type u
β : Type v
γ : Type ?u.514368
δ : Type ?u.514371
ε : Type ?u.514374
ζ : Type ?u.514377
ι : Type u_2
κ : Type ?u.514383
σ : ι → Type u_1
τ : κ → Type ?u.514393
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
s : Set (Sigma σ)
⊢ IsClosed s ↔ ∀ (i : ι), IsClosed (Sigma.mk i ⁻¹' s)
simp only [← isOpen_compl_iff, isOpen_sigma_iff, preimage_compl]