Barycentric coordinates are smooth

theorem contDiff_barycentric_coord {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] (b : AffineBasis ι 𝕜 E) (i : ι) : ContDiff 𝕜 ⊤ ⇑(b.coord i)

@[deprecated contDiff_barycentric_coord (since := "2026-10-17")]

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 : ι) : ContDiff 𝕜 ⊤ ⇑(b.coord i)

Alias of contDiff_barycentric_coord.