Barycentric coordinates are smooth #
theorem
smooth_barycentric_coord
{ι : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[FiniteDimensional 𝕜 E]
(b : AffineBasis ι 𝕜 E)
(i : ι)
: