# Continuity of the functoriality of `X → M` when `X` is finite #

source
theorem FunOnFinite.continuous_map (M : Type u_1) [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {X : Type u_2} {Y : Type u_3} [Finite X] [Finite Y] (f : X → Y) :
Continuous (map f)
source
theorem FunOnFinite.continuous_linearMap (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] {X : Type u_3} {Y : Type u_4} [Finite X] [Finite Y] (f : X → Y) :
Continuous ⇑(linearMap R M f)