Let 𝑋 be a closed convex subset of ℝ^𝑑. Then: • 𝑋 is a 𝑉-polytope if it is the convex hull of a finite point set. • 𝑋 is an 𝐻-polytope if it is the intersection of finitely many half spaces.

Theorem : Every 𝑉-polytope is an 𝐻-polytope, and every compact 𝐻-polytope is a 𝑉-polytope.

theorem hxSegBallInterSeg {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : E} (x1 x2 : E) (ε : ℝ) : x ∈ openSegment ℝ x1 x2 ∧ ¬(x1 = x ∧ x2 = x) → 0 < ε → ∃ (x1' : E) (x2' : E), x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)

def Hpolytope.I {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (H_ : Set (Halfspace E)) (x : E) : Set (Halfspace E)

The halfspaces of H_ whose boundary contains the point x.

Equations

• Hpolytope.I H_ x = {Hi_ : Halfspace E | Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_}

theorem Hpolytope.I_mem {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {H_ : Set (Halfspace E)} (x : E) (Hi_ : Halfspace E) : Hi_ ∈ I H_ x ↔ Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_

theorem Hpolytope.I_sub {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {H_ : Set (Halfspace E)} (x : E) : I H_ x ⊆ H_

theorem ExtremePointsofHpolytope {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {H_ : Set (Halfspace E)} (hH_ : H_.Finite) (x : E) : x ∈ Hpolytope hH_ → (x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun (x : Halfspace E) => frontier ↑x) '' Hpolytope.I H_ x) = {x})

theorem DualOfVpolytope_compactHpolytope {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {S : Set E} (hS : S.Finite) (hS0 : 0 ∈ interior (Vpolytope hS)) : ∃ (H_ : Set (Halfspace E)) (hH_ : H_.Finite), Hpolytope hH_ = polarDual (Vpolytope hS) ∧ IsCompact (Hpolytope hH_)

theorem Vpolytope_of_Hpolytope {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {H_ : Set (Halfspace E)} (hH_ : H_.Finite) : IsCompact (Hpolytope hH_) → ∃ (S : Set E) (hS : S.Finite), Hpolytope hH_ = Vpolytope hS

theorem Hpolytope_of_Vpolytope_subsingleton {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] [Nontrivial E] {S : Set E} (hS : S.Finite) (hStrivial : S.Subsingleton) : ∃ (H_ : Set (Halfspace E)) (hH_ : H_.Finite), Hpolytope hH_ = Vpolytope hS

theorem Hpolytope_of_Vpolytope_0interior {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {S : Set E} (hS : S.Finite) (hV0 : 0 ∈ interior (Vpolytope hS)) : ∃ (H_ : Set (Halfspace E)) (hH_ : H_.Finite), Hpolytope hH_ = Vpolytope hS

def translationHomeo {E : Type} [NormedAddCommGroup E] (x : E) : E ≃ₜ E

Translation by x as a homeomorphism of E.

Equations

• translationHomeo x = { toFun := fun (x_1 : E) => x_1 + x, invFun := fun (x_1 : E) => x_1 + -x, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem translationHomeo.toFun.def {E : Type} [NormedAddCommGroup E] (x : E) : ⇑(translationHomeo x) = fun (x_1 : E) => x_1 + x

theorem Hpolytope_of_Vpolytope_interior {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {S : Set E} (hS : S.Finite) (hVinteriorNonempty : (interior (Vpolytope hS)).Nonempty) : ∃ (H_ : Set (Halfspace E)) (hH_ : H_.Finite), Hpolytope hH_ = Vpolytope hS

theorem Vpolytope_of_Vpolytope_inter_cutSpace_fin {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {S : Set E} (hS : S.Finite) (hVinterior : (interior (Vpolytope hS)).Nonempty) {H_ : Set (Halfspace E)} (hH_ : H_.Finite) : ∃ (S' : Set E) (hS' : S'.Finite), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_

theorem InDown_eq_DownIn {E P : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [PseudoMetricSpace P] [NormedAddTorsor E P] {p : AffineSubspace ℝ P} [Nonempty ↥p] {S : Set P} (x : ↥p) : ⇑(AffineIsometryEquiv.VSubconst ℝ x) '' Subtype.val ⁻¹' S = Subtype.val ⁻¹' (S -ᵥ {↑x})

theorem Nonempty_iff_Nonempty_interior_in_direction {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {S : Set E} {s : E} (hs : s ∈ S) (hS : Nonempty ↑S) : (interior (⇑(AffineIsometryEquiv.VSubconst ℝ ⟨s, ⋯⟩) '' Subtype.val ⁻¹' (convexHull ℝ) S)).Nonempty

theorem MainTheoremOfPolytopes {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] [Nontrivial E] : (∀ (S : Set E) (hS : S.Finite), ∃ (H_ : Set (Halfspace E)) (hH_ : H_.Finite), Hpolytope hH_ = Vpolytope hS) ∧ ∀ {H_ : Set (Halfspace E)} (hH_ : H_.Finite), IsCompact (Hpolytope hH_) → ∃ (S : Set E) (hS : S.Finite), Hpolytope hH_ = Vpolytope hS