M : Type u_4
α✝ : Type ?u.23804
β✝ : Type ?u.23807
inst✝⁹ : TopologicalSpace α✝
inst✝⁸ : Monoid M
inst✝⁷ : MulAction M α✝
inst✝⁶ : ContinuousConstSMul M α✝
N : Type u_1
inst✝⁵ : Monoid N
α : Type u_2
β : Type u_3
inst✝⁴ : MulAction M α
inst✝³ : MulAction N β
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : ContinuousConstSMul N β
σ : M → N
⊢ IsClosed (⋂ (i : M) (i_1 : α), {x | x (i • i_1) = σ i • x i_1})
M : Type u_4
α✝ : Type ?u.23804
β✝ : Type ?u.23807
inst✝⁹ : TopologicalSpace α✝
inst✝⁸ : Monoid M
inst✝⁷ : MulAction M α✝
inst✝⁶ : ContinuousConstSMul M α✝
N : Type u_1
inst✝⁵ : Monoid N
α : Type u_2
β : Type u_3
inst✝⁴ : MulAction M α
inst✝³ : MulAction N β
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : ContinuousConstSMul N β
σ : M → N
⊢ IsClosed {f | ∀ (c : M) (x : α), f (c • x) = σ c • f x}
simp only [Set.setOf_forall]
no goals
M : Type u_4
α✝ : Type ?u.23804
β✝ : Type ?u.23807
inst✝⁹ : TopologicalSpace α✝
inst✝⁸ : Monoid M
inst✝⁷ : MulAction M α✝
inst✝⁶ : ContinuousConstSMul M α✝
N : Type u_1
inst✝⁵ : Monoid N
α : Type u_2
β : Type u_3
inst✝⁴ : MulAction M α
inst✝³ : MulAction N β
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : ContinuousConstSMul N β
σ : M → N
⊢ IsClosed (⋂ (i : M) (i_1 : α), {x | x (i • i_1) = σ i • x i_1})
exact isClosed_iInter fun c => isClosed_iInter fun x =>
  isClosed_eq (continuous_apply _) ((continuous_apply _).const_smul _)