English
A subset s of a topological real vector space is ample precisely when, for every x in s, the convex hull of the connected component of x inside s is the whole space.
Русский
Подмножество s топологического вещественного векторного пространства называется ампельным тогда и лишь тогда, когда для каждого x ∈ sConvexHull(соединенной компоненты x внутри s) совпадает с whole space.
LaTeX
$$$\mathrm{AmpleSet}(s)\;\Longleftrightarrow\; \forall x\in s,\; \mathrm{convexHull}_{\mathbb{R}}(\mathrm{connectedComponentIn}(s,x)) = \mathrm{univ}$$$
Lean4
/-- A subset of a topological real vector space is ample
if the convex hull of each of its connected components is the full space. -/
def AmpleSet (s : Set F) : Prop :=
∀ x ∈ s, convexHull ℝ (connectedComponentIn s x) = univ
