Polytopes #
We define polytopes as convex hulls of finite sets.
def
IsPolytope
(R : Type u_1)
{E : Type u_3}
[Semiring R]
[PartialOrder R]
[AddCommMonoid E]
[Module R E]
(s : Set E)
:
A set is a polytope if it is the convex hull of finitely many points.
Equations
- IsPolytope R s = ∃ (t : Finset E), s = (convexHull R) ↑t
Instances For
@[simp]
theorem
IsPolytope.empty
{R : Type u_1}
{E : Type u_3}
[Semiring R]
[PartialOrder R]
[AddCommMonoid E]
[Module R E]
:
IsPolytope R ∅
@[simp]
theorem
IsPolytope.singleton
{R : Type u_1}
{E : Type u_3}
[Semiring R]
[PartialOrder R]
[AddCommMonoid E]
[Module R E]
{x : E}
:
IsPolytope R {x}
@[simp]
theorem
IsPolytope.segment
{R : Type u_1}
{E : Type u_3}
[Semiring R]
[PartialOrder R]
[AddCommMonoid E]
[Module R E]
{x y : E}
[IsOrderedRing R]
:
IsPolytope R (segment R x y)
@[simp]
theorem
IsPolytope.convexHull_finset
{R : Type u_1}
{E : Type u_3}
[Semiring R]
[PartialOrder R]
[AddCommMonoid E]
[Module R E]
{s : Finset E}
:
IsPolytope R ((convexHull R) ↑s)
theorem
IsPolytope.neg
{R : Type u_1}
{E : Type u_3}
[Ring R]
[PartialOrder R]
[AddCommGroup E]
[Module R E]
{s : Set E}
:
IsPolytope R s → IsPolytope R (-s)
theorem
IsPolytope.add
{𝕜 : Type u_2}
{E : Type u_3}
[Field 𝕜]
[LinearOrder 𝕜]
[IsStrictOrderedRing 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
{s t : Set E}
:
IsPolytope 𝕜 s → IsPolytope 𝕜 t → IsPolytope 𝕜 (s + t)
theorem
IsPolytope.sub
{𝕜 : Type u_2}
{E : Type u_3}
[Field 𝕜]
[LinearOrder 𝕜]
[IsStrictOrderedRing 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
{s t : Set E}
(hs : IsPolytope 𝕜 s)
(ht : IsPolytope 𝕜 t)
:
IsPolytope 𝕜 (s - t)