Theorems · Theorem · functional analysis

AffineBasis.interior_convexHull

∀ {ι : Type u_1} {E : Type u_2} [Finite ι] [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  (b : AffineBasis ι ℝ E), interior ((convexHull ℝ) (Set.range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}

Given a finite-dimensional normed real vector space, the interior of the convex hull of an affine basis is the set of points whose barycentric coordinates are strictly positive with respect to this basis. TODO Restate this result for affine spaces (instead of vector spaces) once the definition of convexity is generalised to this setting.

Defined in

Mathlib.Analysis.Normed.Affine.AddTorsorBases

Cited by

1 results in Mathlib

Foundations

Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FiniteNormedAddCommGroupNormedSpace