α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : InvolutiveInv G
inst✝ : ContinuousInv G
s : Set G
hs : IsCompact s
⊢ IsCompact (Inv.inv '' s)
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : InvolutiveInv G
inst✝ : ContinuousInv G
s : Set G
hs : IsCompact s
⊢ IsCompact s⁻¹
rw [← image_inv]
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : InvolutiveInv G
inst✝ : ContinuousInv G
s : Set G
hs : IsCompact s
⊢ IsCompact (Inv.inv '' s)
exact hs.image continuous_inv