α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Inv G
inst✝⁶ : ContinuousInv G
inst✝⁵ : TopologicalSpace α
f : α → G
s : Set α
x : α
ι : Type ?u.28517
G₁ : Type u_1
G₂ : Type u_2
inst✝⁴ : TopologicalSpace G₂
inst✝³ : T2Space G₂
inst✝² : Inv G₁
inst✝¹ : Inv G₂
inst✝ : ContinuousInv G₂
⊢ IsClosed (⋂ (i : G₁), {x | x i⁻¹ = (x i)⁻¹})
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Inv G
inst✝⁶ : ContinuousInv G
inst✝⁵ : TopologicalSpace α
f : α → G
s : Set α
x : α
ι : Type ?u.28517
G₁ : Type u_1
G₂ : Type u_2
inst✝⁴ : TopologicalSpace G₂
inst✝³ : T2Space G₂
inst✝² : Inv G₁
inst✝¹ : Inv G₂
inst✝ : ContinuousInv G₂
⊢ IsClosed {f | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}
simp only [setOf_forall]
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Inv G
inst✝⁶ : ContinuousInv G
inst✝⁵ : TopologicalSpace α
f : α → G
s : Set α
x : α
ι : Type ?u.28517
G₁ : Type u_1
G₂ : Type u_2
inst✝⁴ : TopologicalSpace G₂
inst✝³ : T2Space G₂
inst✝² : Inv G₁
inst✝¹ : Inv G₂
inst✝ : ContinuousInv G₂
⊢ IsClosed (⋂ (i : G₁), {x | x i⁻¹ = (x i)⁻¹})
refine' isClosed_iInter fun i => isClosed_eq (continuous_apply _) (continuous_apply _).inv