Continuity of affine maps between standard simplices

An affine map Convexity.StdSimplex.affineMapMk v out of a standard simplex is determined by the images v m of the vertices. When the target is a standard simplex on a finite type, its weights are the bilinear expressions ∑ m, w.weights m * (v m).weights n, so the map is continuous; Convexity.StdSimplex.continuousAffineMapMk bundles it as a continuous map. This makes affine simplices, such as the simplices of a barycentric subdivision, available as continuous maps between topological standard simplices.

@[simp]

theorem Convexity.StdSimplex.weights_affineMapMk_apply {R : Type u_1} [PartialOrder R] {M : Type u_2} {N : Type u_3} [Semiring R] [IsStrictOrderedRing R] [Fintype M] (v : M → StdSimplex R N) (w : StdSimplex R M) (n : N) : ((affineMapMk v) w).weights n = ∑ m : M, w.weights m * (v m).weights n

The weights of the affine map with vertices v, evaluated at a point with finitely many vertices, are the corresponding convex combinations of the weights of the vertices.

theorem Convexity.StdSimplex.continuous_affineMapMk {R : Type u_1} [PartialOrder R] {M : Type u_2} {N : Type u_3} [Ring R] [IsStrictOrderedRing R] [TopologicalSpace R] [IsTopologicalRing R] [Finite N] (v : M → StdSimplex R N) : Continuous ⇑(affineMapMk v)

An affine map from a standard simplex to a standard simplex on a finite type is continuous.

noncomputable def Convexity.StdSimplex.continuousAffineMapMk {R : Type u_1} [PartialOrder R] {M : Type u_2} {N : Type u_3} [Ring R] [IsStrictOrderedRing R] [TopologicalSpace R] [IsTopologicalRing R] [Finite N] (v : M → StdSimplex R N) : C(StdSimplex R M, StdSimplex R N)

The affine map with vertices v from a standard simplex to a standard simplex on a finite type, as a continuous map.

Equations

• Convexity.StdSimplex.continuousAffineMapMk v = { toFun := ⇑(Convexity.StdSimplex.affineMapMk v), continuous_toFun := ⋯ }

@[simp]

theorem Convexity.StdSimplex.continuousAffineMapMk_apply {R : Type u_1} [PartialOrder R] {M : Type u_2} {N : Type u_3} [Ring R] [IsStrictOrderedRing R] [TopologicalSpace R] [IsTopologicalRing R] [Finite N] (v : M → StdSimplex R N) (w : StdSimplex R M) : (continuousAffineMapMk v) w = (affineMapMk v) w