OAI/GroupTheory/PolycyclicRecognition/Analysis/CompactFiniteDimensionalHull.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Compact convex hulls in the finite character space

Only dimension-plus-one tuples are needed, by Carathéodory. Their coefficient simplex and their point tuples are compact, so their finite union is compact.

  1. def OAI.PolycyclicRecognition.finiteConvexCombinationRange line 19
  2. theorem OAI.PolycyclicRecognition.finiteConvexCombinationRange_compact line 23
  3. theorem OAI.PolycyclicRecognition.finiteConvexCombinationRange_subset line 29
  4. theorem OAI.PolycyclicRecognition.mem_small_finiteConvexCombinationRange line 36
  5. theorem OAI.PolycyclicRecognition.compact_finiteDimensional_convexHull line 56