English
For a finite-dimensional real vector space, the interior of the convex hull is nonempty if and only if the affine span is the whole space.
Русский
Для конечномерного вещественного пространства interior(convexHull) непусто тогда, когда аффинное порождение равно пространству.
LaTeX
$$$$\big(\operatorname{interior}(\operatorname{convexHull}_{\mathbb{R}} s)\big) \neq \varnothing \iff \operatorname{affineSpan}_{\mathbb{R}} s = \top.$$$$
Lean4
theorem interior_convexHull_nonempty_iff_affineSpan_eq_top [FiniteDimensional ℝ V] {s : Set V} :
(interior (convexHull ℝ s)).Nonempty ↔ affineSpan ℝ s = ⊤ :=
by
refine ⟨affineSpan_eq_top_of_nonempty_interior, fun h => ?_⟩
obtain ⟨t, hts, b, hb⟩ := AffineBasis.exists_affine_subbasis h
suffices (interior (convexHull ℝ (range b))).Nonempty
by
rw [hb, Subtype.range_coe_subtype, setOf_mem_eq] at this
refine this.mono (by gcongr)
lift t to Finset V using b.finite_set
exact ⟨_, b.centroid_mem_interior_convexHull⟩
