English
Let X and Y be finite types and M a topological R-module. For any function f: X → Y, the linear map on function spaces L_f that precomposes with f, L_f: M^Y → M^X given by (L_f(φ))(x) = φ(f(x)), is continuous (hence a continuous linear map).
Русский
Пусть X и Y — конечные множества, M — топологический модуль над R. При любом отображении f: X → Y линейное отображение между пространствами функций L_f: M^Y → M^X, задающее (L_f(φ))(x) = φ(f(x)), непрерывно.
LaTeX
$$$L_f: M^Y \to M^X,\quad (L_f(\varphi))(x)=\varphi(f(x)).$$$
Lean4
theorem continuous_linearMap (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M]
[ContinuousAdd M] {X Y : Type*} [Finite X] [Finite Y] (f : X → Y) : Continuous (FunOnFinite.linearMap R M f) :=
FunOnFinite.continuous_map _ _
