no goals
α : Type u
β : Type v
ι : Type ?u.94686
π : ι → Type ?u.94691
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
⊢ IsCompact s ↔ IsCompact univ
rw [isCompact_iff_isCompact_in_subtype, image_univ, Subtype.range_coe]