no goals
α : Type u
β : Type v
γ : Type ?u.119189
δ : Type ?u.119192
ε : Type ?u.119195
ζ : Type ?u.119198
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s : Set (α ⊕ β)
⊢ IsClosed s ↔ IsClosed (inl ⁻¹' s) ∧ IsClosed (inr ⁻¹' s)
simp only [← isOpen_compl_iff, isOpen_sum_iff, preimage_compl]