smooth_barycentric_coord — Mathlib

English

Let b be an affine basis of E. For each i, the i-th barycentric coordinate function coord_i is C^∞ (ContDiff) on E with target 𝕜.

Русский

Пусть b — аффинная базисная система. Для каждого i функция координаты барицентра coord_i гладкая:，它 принадлежит C^∞(E, 𝕜).

LaTeX

$$$ \operatorname{ContDiff}_{\mathbb{k}}(\top)(b.coord_i). $$$

Lean4

theorem smooth_barycentric_coord (b : AffineBasis ι 𝕜 E) (i : ι) : ContDiff 𝕜 ⊤ (b.coord i) :=
  (⟨b.coord i, continuous_barycentric_coord b i⟩ : E →ᴬ[𝕜] 𝕜).contDiff

Похожие утверждения