Continuity of affine maps from the standard simplex to modules

theorem Convexity.StdSimplex.continuous_of_affineMap {R : Type u_1} {E : Type u_2} {ι : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [ConvexSpace R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace R] [IsTopologicalRing R] [ContinuousSMul R E] [IsModuleConvexSpace R E] (f : ConvexSpace.AffineMap R (StdSimplex R ι) E) : Continuous ⇑f

theorem Convexity.StdSimplex.continuous_of_isAffineMap {R : Type u_1} {E : Type u_2} {ι : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [ConvexSpace R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace R] [IsTopologicalRing R] [ContinuousSMul R E] [IsModuleConvexSpace R E] (f : StdSimplex R ι → E) (hf : IsAffineMap R f) : Continuous f