English
If ι is finite, a linear map f: (ι → R) → M is continuous with respect to the product topology, by expressing it in a basis and using the continuity of coordinate maps.
Русский
Для конечного множества индексов ι линейное отображение f с виду непрерывно по произведенной топологии, выражая через базис и непрерывность координат.
LaTeX
$$$f: (ι \to R) \to M \text{ continuous when } ι \text{ finite}$$$
Lean4
theorem continuous_on_pi {ι : Type*} {R : Type*} {M : Type*} [Finite ι] [Semiring R] [TopologicalSpace R]
[AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousSMul R M] (f : (ι → R) →ₗ[R] M) :
Continuous f := by
cases nonempty_fintype ι
classical
-- for the proof, write `f` in the standard basis, and use that each coordinate is a continuous
-- function.
have : (f : (ι → R) → M) = fun x => ∑ i : ι, x i • f fun j => if i = j then 1 else 0 :=
by
ext x
exact f.pi_apply_eq_sum_univ x
rw [this]
refine continuous_finset_sum _ fun i _ => ?_
exact (continuous_apply i).smul continuous_const
