ι : Type ?u.64907
α : Type ?u.64910
X : Type ?u.64913
M : Type ?u.64916
N : Type ?u.64919
inst✝⁵ : TopologicalSpace X
M₁ : Type u_1
M₂ : Type u_2
inst✝⁴ : TopologicalSpace M₂
inst✝³ : T2Space M₂
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : ContinuousMul M₂
⊢ IsClosed (⋂ (i : M₁) (i_1 : M₁), {x | x (i * i_1) = x i * x i_1})
ι : Type ?u.64907
α : Type ?u.64910
X : Type ?u.64913
M : Type ?u.64916
N : Type ?u.64919
inst✝⁵ : TopologicalSpace X
M₁ : Type u_1
M₂ : Type u_2
inst✝⁴ : TopologicalSpace M₂
inst✝³ : T2Space M₂
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : ContinuousMul M₂
⊢ IsClosed {f | ∀ (x y : M₁), f (x * y) = f x * f y}
simp only [setOf_forall]
no goals
ι : Type ?u.64907
α : Type ?u.64910
X : Type ?u.64913
M : Type ?u.64916
N : Type ?u.64919
inst✝⁵ : TopologicalSpace X
M₁ : Type u_1
M₂ : Type u_2
inst✝⁴ : TopologicalSpace M₂
inst✝³ : T2Space M₂
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : ContinuousMul M₂
⊢ IsClosed (⋂ (i : M₁) (i_1 : M₁), {x | x (i * i_1) = x i * x i_1})
exact
  isClosed_iInter fun x =>
    isClosed_iInter fun y =>
      isClosed_eq (continuous_apply _)
        (by continuity)
no goals
ι : Type ?u.64907
α : Type ?u.64910
X : Type ?u.64913
M : Type ?u.64916
N : Type ?u.64919
inst✝⁵ : TopologicalSpace X
M₁ : Type u_1
M₂ : Type u_2
inst✝⁴ : TopologicalSpace M₂
inst✝³ : T2Space M₂
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : ContinuousMul M₂
x y : M₁
⊢ Continuous fun x_1 => x_1 x * x_1 y
continuity