English
The set of functions f: α → β satisfying f(c • x) = σ(c) • f(x) for all c ∈ M and x ∈ α is a closed subset of the function space β^α (with the product topology).
Русский
Множество функций f: α → β, удовлетворяющих f(c • x) = σ(c) • f(x) для всех c ∈ M и x ∈ α, замкнуто в пространстве функций β^α (с произведной топологией).
LaTeX
$$$ \\text{IsClosed}\\bigl\\{ f : \\alpha \\to \\beta \\mid \\forall c\\,x,\\ f(c \\cdot x) = \\sigma c \\cdot f x \\bigr\\} $$$
Lean4
theorem isClosed_setOf_map_smul {N : Type*} [Monoid N] (α β) [MulAction M α] [MulAction N β] [TopologicalSpace β]
[T2Space β] [ContinuousConstSMul N β] (σ : M → N) : IsClosed {f : α → β | ∀ c x, f (c • x) = σ c • f x} :=
by
simp only [Set.setOf_forall]
exact
isClosed_iInter fun c =>
isClosed_iInter fun x => isClosed_eq (continuous_apply _) ((continuous_apply _).const_smul _)
