Theorems · Theorem · convex and discrete geometry

Set.Finite.isClosed_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] [T2Space E]
  {s : Set E}, s.Finite → IsClosed ((convexHull 𝕜) s)

Convex hull of a finite set is closed.

Defined in

Mathlib.Analysis.Convex.Topology

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRingTopologicalSpaceOrderClosedTopologyCompactIccSpaceContinuousAddAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMulT2Space