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)
: