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

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)

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)