Theorems · Theorem · convex and discrete geometry

Set.Finite.isCompact_convexHull

∀ {E : Type u_3} (𝕜 : Type u_4) [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderClosedTopology 𝕜] [CompactIccSpace 𝕜] [ContinuousAdd 𝕜] [inst_7 : AddCommGroup E]
  [inst_8 : Module 𝕜 E] [inst_9 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {s : Set E},
  s.Finite → IsCompact ((convexHull 𝕜) s)

Convex hull of a finite set is compact.

Defined in

Mathlib.Analysis.Convex.Topology

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRingTopologicalSpaceOrderClosedTopologyCompactIccSpaceContinuousAddAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMul