Theorems · Definition · convex and discrete geometry

AmpleSet

{F : Type u_1} → [inst : AddCommGroup F] → [Module ℝ F] → [TopologicalSpace F] → Set F → Prop

A subset of a topological real vector space is ample if the convex hull of each of its connected components is the full space.

Defined in

Mathlib.Analysis.Convex.AmpleSet

Cited by

10 results in Mathlib

Foundations

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

Assumes

AddCommGroupModuleTopologicalSpace