continuous_barycentric_coord — Mathlib

English

For a finite-dimensional real vector space E and an affine basis b, each coordinate function coord i is continuous.

Русский

Для конечномерного вещественного пространства E и аффинной базы b каждая координатная функция coord i непрерывна.

LaTeX

$$$$\text{Continuous}(b.coord(i)).$$$$

Lean4

@[continuity]
theorem continuous_barycentric_coord (i : ι) : Continuous (b.coord i) :=
  (b.coord i).continuous_of_finiteDimensional

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