affineSpan_eq_top_of_nonempty_interior

English

The interior of the convex hull of an affine basis is characterized by positive barycentric coordinates.

Русский

interior(convexHull( range b)) определяется положительными барицентрическими координатами относительно базы b.

LaTeX

$$$$\text{Interior}(\operatorname{convexHull}_{\mathbb{R}}(\operatorname{range}(b))) = \{x \mid ∀ i, 0 < b.coord(i)x\}.$$$$

Lean4

theorem affineSpan_eq_top_of_nonempty_interior {s : Set V} (hs : (interior <| convexHull ℝ s).Nonempty) :
    affineSpan ℝ s = ⊤ :=
  top_unique <|
    isOpen_interior.affineSpan_eq_top hs ▸ (affineSpan_mono _ interior_subset).trans_eq (affineSpan_convexHull _)

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