theorem mem_euclideanRelativeInterior_mixedConvexHull_range_of_strict_mixedConvexCombination {n k m : ℕ} {x : Fin n → ℝ} (p : Fin k → Fin n → ℝ) (d : Fin m → Fin n → ℝ) (a : Fin k → ℝ) (b : Fin m → ℝ) (ha : ∀ (i : Fin k), 0 < a i) (hb : ∀ (j : Fin m), 0 < b j) (hsum : ∑ i : Fin k, a i = 1) (hx : x = ∑ i : Fin k, a i • p i + ∑ j : Fin m, b j • d j) : x ∈ euclideanRelativeInterior_fin n (mixedConvexHull (Set.range p) (Set.range d))

A strict mixed convex combination lies in the relative interior of its mixed convex hull.

theorem subset_of_isFace_of_convex_of_euclideanRelativeInterior_fin_inter {n : ℕ} {C C' D : Set (Fin n → ℝ)} (hC' : IsFace C C') (hDC : D ⊆ C) (hri : (euclideanRelativeInterior_fin n D ∩ C').Nonempty) : D ⊆ C'

Theorem 18.1 in Fin n → ℝ using euclideanRelativeInterior_fin.

theorem face_mixedConvexHull_eq_mixedConvexHull_inter_recessionCone {n : ℕ} (S₀ S₁ : Set (Fin n → ℝ)) {C' : Set (Fin n → ℝ)} (hC' : IsFace (mixedConvexHull S₀ S₁) C') (hC'conv : Convex ℝ C') : C' = mixedConvexHull (S₀ ∩ C') (S₁ ∩ C'.recessionCone)

Theorem 18.3. Let C = conv S, where S is a set of points and directions, and let C' be a non-empty face of C. Then C' = conv S', where S' consists of the points in S which belong to C' and the directions in S which are directions of recession of C'.

theorem isFace_singleton_of_isExtremePoint_mixedConvexHull {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} {x : Fin n → ℝ} (hx : IsExtremePoint (mixedConvexHull S₀ S₁) x) : IsFace (mixedConvexHull S₀ S₁) {x}

A singleton face arises from an extreme point of a mixed convex hull.

theorem mem_points_of_isExtremePoint_mixedConvexHull {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} {x : Fin n → ℝ} : IsExtremePoint (mixedConvexHull S₀ S₁) x → x ∈ S₀

Corollary 18.3.1. Suppose C = conv S, where S is given as a set of points S₀ and directions S₁ (so here C = mixedConvexHull S₀ S₁). Then every extreme point of C is a point of S (i.e. lies in S₀).

theorem convex_ray_image {n : ℕ} (x d : Fin n → ℝ) : Convex ℝ ((fun (t : ℝ) => x + t • d) '' Set.Ici 0)

A half-line {x + t • d | t ≥ 0} is convex.

theorem ray_image_nonempty {n : ℕ} (x d : Fin n → ℝ) : ((fun (t : ℝ) => x + t • d) '' Set.Ici 0).Nonempty

A half-line {x + t • d | t ≥ 0} is nonempty.

theorem recessionCone_ray_eq_rayNonneg_singleton {n : ℕ} (x d : Fin n → ℝ) : ((fun (t : ℝ) => x + t • d) '' Set.Ici 0).recessionCone = rayNonneg n {d}

The recession cone of a half-line is the nonnegative ray of its direction.

theorem mem_rayNonneg_of_exists_pos_smul_mem {n : ℕ} {S₁ : Set (Fin n → ℝ)} {d : Fin n → ℝ} (h : ∃ s ∈ S₁, ∃ (a : ℝ), 0 < a ∧ s = a • d) : d ∈ rayNonneg n S₁

If a positive multiple of d lies in S₁, then d lies in rayNonneg n S₁.

theorem not_isBounded_ray_image_of_ne_zero {n : ℕ} {x d : Fin n → ℝ} (hd : d ≠ 0) : ¬Bornology.IsBounded ((fun (t : ℝ) => x + t • d) '' Set.Ici 0)

A nonzero ray {x + t • d | t ≥ 0} is unbounded.

theorem cone_eq_singleton_zero_of_subset {n : ℕ} {S : Set (Fin n → ℝ)} (hS : S ⊆ {0}) : cone n S = {0}

If a direction set is contained in {0}, its cone is {0}.

theorem exists_ne_zero_mem_S₁_inter_recessionCone_of_face_ray {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} {x d : Fin n → ℝ} (hd : d ≠ 0) (hface : IsFace (mixedConvexHull S₀ S₁) ((fun (t : ℝ) => x + t • d) '' Set.Ici 0)) (hconv : Convex ℝ ((fun (t : ℝ) => x + t • d) '' Set.Ici 0)) (hNoUnbounded : ∀ (x d' : Fin n → ℝ), (fun (t : ℝ) => x + t • d') '' Set.Ici 0 ⊆ mixedConvexHull S₀ S₁ → Bornology.IsBounded (S₀ ∩ (fun (t : ℝ) => x + t • d') '' Set.Ici 0)) : ∃ s ∈ S₁ ∩ ((fun (t : ℝ) => x + t • d) '' Set.Ici 0).recessionCone, s ≠ 0

A half-line face of a mixed convex hull yields a nonzero direction from S₁.

theorem mem_directions_of_isExtremeDirection_mixedConvexHull {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} {d : Fin n → ℝ} (hNoUnbounded : ∀ (x d' : Fin n → ℝ), (fun (t : ℝ) => x + t • d') '' Set.Ici 0 ⊆ mixedConvexHull S₀ S₁ → Bornology.IsBounded (S₀ ∩ (fun (t : ℝ) => x + t • d') '' Set.Ici 0)) : IsExtremeDirection (mixedConvexHull S₀ S₁) d → d ∈ rayNonneg n S₁

Corollary 18.3.1. Suppose C = conv S, where S is given as a set of points S₀ and directions S₁ (so C = mixedConvexHull S₀ S₁). If no half-line in C contains an unbounded set of points of S (i.e. along any ray contained in C, the subset of points from S₀ is bounded), then every extreme direction of C is a nonnegative multiple of a direction in S₁.

theorem add_sub_mem_of_mem_linealitySpace {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hC : Convex ℝ C) {v x : EuclideanSpace ℝ (Fin n)} (hv : v ∈ C.linealitySpace) (hx : x ∈ C) : x + v ∈ C ∧ x - v ∈ C

Lineality directions translate points of a convex set.

theorem mem_openSegment_add_sub_half {n : ℕ} (x v : EuclideanSpace ℝ (Fin n)) : x ∈ openSegment ℝ (x + v) (x - v)

The midpoint of x + v and x - v lies in their open segment.

theorem not_mem_extremePoints_of_exists_nonzero_lineality {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hC : Convex ℝ C) {v : EuclideanSpace ℝ (Fin n)} (hv0 : v ≠ 0) (hvL : v ∈ C.linealitySpace) (x : EuclideanSpace ℝ (Fin n)) : x ∉ Set.extremePoints ℝ C

A nonzero lineality direction prevents extreme points.

theorem extremePoints_eq_empty_of_linealitySpace_nontrivial {n : ℕ} (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (hL : ∃ (y : EuclideanSpace ℝ (Fin n)), y ≠ 0 ∧ y ∈ C.linealitySpace) : Set.extremePoints ℝ C = ∅

Text 18.3.1. If the lineality space L of a convex set C is non-zero (equivalently: C contains at least one line), then C has no extreme points.

theorem euclideanRelativeBoundary_eq_diff_of_isClosed {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hC : IsClosed C) : euclideanRelativeBoundary n C = C \ euclideanRelativeInterior n C

For a closed set, the relative boundary is C \ ri C.

theorem exists_two_rb_points_with_ri_point_on_openSegment {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hnotconv : ¬Convex ℝ (euclideanRelativeBoundary n C)) : ∃ (x₁ : EuclideanSpace ℝ (Fin n)) (x₂ : EuclideanSpace ℝ (Fin n)), x₁ ∈ euclideanRelativeBoundary n C ∧ x₂ ∈ euclideanRelativeBoundary n C ∧ x₁ ≠ x₂ ∧ ∃ y ∈ euclideanRelativeInterior n C, y ∈ openSegment ℝ x₁ x₂

From nonconvex relative boundary, pick boundary endpoints with a relative interior point on their open segment.

theorem exists_rb_point_on_segment_of_mem_ri_of_not_mem {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCclosed : IsClosed C) {y x : EuclideanSpace ℝ (Fin n)} (hy : y ∈ euclideanRelativeInterior n C) (hxaff : x ∈ affineSpan ℝ C) (hxC : x ∉ C) : ∃ z ∈ euclideanRelativeBoundary n C, z ∈ openSegment ℝ y x

If y ∈ ri C and x ∈ aff C lies outside C, then the open segment y–x meets rb C.

theorem euclideanRelativeBoundary_nonempty_of_isClosed_convex_of_not_affine {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hCne : C.Nonempty) (hC_not_affine : ¬∃ (A : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))), ↑A = C) : (euclideanRelativeBoundary n C).Nonempty

A closed convex set that is not affine has nonempty relative boundary.

theorem exists_supportingHyperplane_data_of_convex_rb {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hDconv : Convex ℝ (euclideanRelativeBoundary n C)) (hDne : (euclideanRelativeBoundary n C).Nonempty) : ∃ (f : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] ℝ) (a : ℝ), f ≠ 0 ∧ (∀ x ∈ C, f x ≤ a) ∧ (∀ x ∈ euclideanRelativeBoundary n C, f x = a) ∧ ∃ x0 ∈ C, f x0 < a

Convexity of the relative boundary yields supporting hyperplane data.

theorem not_convex_euclideanRelativeBoundary_of_not_affine_not_closedHalf {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hCne : C.Nonempty) (hC_not_affine : ¬∃ (A : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))), ↑A = C) (hC_not_closedHalf_affine : ¬∃ (A : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) (f : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] ℝ) (a : ℝ), f ≠ 0 ∧ C = ↑A ∩ {x : EuclideanSpace ℝ (Fin n) | f x ≤ a}) : ¬Convex ℝ (euclideanRelativeBoundary n C)

The relative boundary of a closed convex set is not convex under the non-affine and non-closed-halfspace hypotheses.

theorem isBounded_segment {n : ℕ} (x₁ x₂ : EuclideanSpace ℝ (Fin n)) : Bornology.IsBounded (segment ℝ x₁ x₂)

A line segment in Euclidean space is bounded.

theorem exists_add_sub_mem_of_mem_ri_of_mem_direction {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} {x v : EuclideanSpace ℝ (Fin n)} (hx : x ∈ euclideanRelativeInterior n C) (hv : v ∈ (affineSpan ℝ C).direction) : ∃ (ε : ℝ), 0 < ε ∧ x + ε • v ∈ C ∧ x - ε • v ∈ C

A relative interior point allows a small step in any affine-span direction.