α : Type u
β : Type v
G : Type w
H : Type x
ι' : Sort u_1
inst✝ : Inv G
ts' : ι' → TopologicalSpace G
h' : ∀ (i : ι'), ContinuousInv G
⊢ ContinuousInv G
α : Type u
β : Type v
G : Type w
H : Type x
ι' : Sort u_1
inst✝ : Inv G
ts' : ι' → TopologicalSpace G
h' : ∀ (i : ι'), ContinuousInv G
⊢ ContinuousInv G
rw [← sInf_range]
no goals
α : Type u
β : Type v
G : Type w
H : Type x
ι' : Sort u_1
inst✝ : Inv G
ts' : ι' → TopologicalSpace G
h' : ∀ (i : ι'), ContinuousInv G
⊢ ContinuousInv G
exact continuousInv_sInf (Set.forall_range_iff.mpr h')