no goals
α : Type ?u.18470
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.18489
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
⊢ IsClosed s ↔ ∀ (i : ι), IsClosed (Subtype.val ⁻¹' s)
simpa using isOpen_iff_coe_preimage_of_iSup_eq_top hU (sᶜ)