isOpenMap_barycentric_coord — Mathlib

English

For any index i, the barycentric coordinate map coord i associated to an affine basis is an open map.

Русский

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

LaTeX

$$$$IsOpenMap\bigl(b.coord(i)\bigr).$$$$

Lean4

theorem isOpenMap_barycentric_coord [Nontrivial ι] (b : AffineBasis ι 𝕜 P) (i : ι) : IsOpenMap (b.coord i) :=
  AffineMap.isOpenMap_linear_iff.mp <|
    (b.coord i).linear.isOpenMap_of_finiteDimensional <| (b.coord i).linear_surjective_iff.mpr (b.surjective_coord i)

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