Affine interpolation on independent points

Arbitrary values on an affinely independent set in a finite-dimensional normed affine space over a complete nontrivially normed field extend to a continuous affine map. In particular, an affine map that is injective on a set with affinely independent image has a continuous affine left inverse on the affine span of that set, hence on its convex hull. This allows inverse simplicial maps to be checked one simplex at a time.

The construction extends the independent set to an affine basis and uses Mathlib's continuous barycentric coordinates. See Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 1, for affine maps of simplices.

theorem AffineIndependent.exists_continuousAffineMap_eqOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {V : Type u_2} {P : Type u_3} {F : Type u_4} [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [MetricSpace P] [NormedAddTorsor V P] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] {s : Set P} (hs : AffineIndependent 𝕜 Subtype.val) (f : P → F) : ∃ (A : P →ᴬ[𝕜] F), Set.EqOn (⇑A) f s

Values on an affinely independent set extend to a continuous affine map of the ambient space. The set need not span the ambient space, and may be empty.

theorem AffineMap.exists_leftInvOn_affineSpan {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {V : Type u_3} {P : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [MetricSpace P] [NormedAddTorsor V P] {s : Set E} (A : E →ᵃ[𝕜] P) (hA : AffineIndependent 𝕜 Subtype.val) (hinj : Set.InjOn (⇑A) s) : ∃ (B : P →ᴬ[𝕜] E), Set.LeftInvOn ⇑B ⇑A ↑(affineSpan 𝕜 s)

An affine map that is injective on a set whose image is affinely independent has a continuous affine left inverse on the affine span of that set.