theorem helperForTheorem_19_1_IsDirectionOf_posMul_of_same_halfLine {n : ℕ} {C' : Set (Fin n → ℝ)} {d d0 : Fin n → ℝ} (hd : IsDirectionOf C' d) (hd0 : IsDirectionOf C' d0) : ∃ (t : ℝ), 0 < t ∧ d = t • d0

Helper for Theorem 19.1: directions of the same half-line are positive multiples.

theorem helperForTheorem_19_1_finiteFaces_imp_exists_finite_direction_reps {n : ℕ} {C : Set (Fin n → ℝ)} : {F : Set (Fin n → ℝ) | IsFace C F}.Finite → ∃ (S₁ : Set (Fin n → ℝ)), S₁.Finite ∧ (∀ (d : Fin n → ℝ), IsExtremeDirection C d → ∃ d0 ∈ S₁, ∃ (t : ℝ), 0 < t ∧ d = t • d0) ∧ S₁ ⊆ {d : Fin n → ℝ | IsExtremeDirection C d}

Helper for Theorem 19.1: finite faces give finitely many direction representatives.

theorem helperForTheorem_19_1_mixedConvexHull_directionSet_eq_of_posMul_cover {n : ℕ} {S₀ S₁ S₁' : Set (Fin n → ℝ)} (hS₁ : S₁ ⊆ S₁') (hpos : ∀ d ∈ S₁', ∃ d0 ∈ S₁, ∃ (t : ℝ), 0 < t ∧ d = t • d0) : mixedConvexHull S₀ S₁' = mixedConvexHull S₀ S₁

Helper for Theorem 19.1: replace direction sets by positive-multiple representatives.

theorem helperForTheorem_19_1_closed_finiteFaces_eq_mixedConvexHull_extremePoints_extremeDirections {n : ℕ} {C : Set (Fin n → ℝ)} (hc : Convex ℝ C) (hclosed : IsClosed C) (hNoLines : ¬∃ (y : Fin n → ℝ), y ≠ 0 ∧ y ∈ -C.recessionCone ∩ C.recessionCone) : C = mixedConvexHull {x : Fin n → ℝ | IsExtremePoint C x} {d : Fin n → ℝ | IsExtremeDirection C d}

Helper for Theorem 19.1: closed convex sets with no lines equal the mixed convex hull of their extreme points and extreme directions.

@[reducible, inline]

abbrev linealitySpace_fin {n : ℕ} (C : Set (Fin n → ℝ)) : Set (Fin n → ℝ)

Helper for Theorem 19.1: lineality space in Fin n → ℝ.

Equations

• linealitySpace_fin C = -C.recessionCone ∩ C.recessionCone

theorem helperForTheorem_19_1_linealitySpace_isSubmodule {n : ℕ} {C : Set (Fin n → ℝ)} (hCconv : Convex ℝ C) : ∃ (L : Submodule ℝ (Fin n → ℝ)), ↑L = linealitySpace_fin C

Helper for Theorem 19.1: the lineality space is a submodule in Fin n → ℝ.

theorem helperForTheorem_19_1_add_sub_mem_of_mem_linealitySpace_fin {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) {v x : Fin n → ℝ} (hv : v ∈ linealitySpace_fin C) (hx : x ∈ C) : x + v ∈ C ∧ x - v ∈ C

Helper for Theorem 19.1: lineality directions translate points in Fin n → ℝ.

theorem helperForTheorem_19_1_linealitySplit_projection_setup {n : ℕ} {C : Set (Fin n → ℝ)} (hc : Convex ℝ C) (hCne : C.Nonempty) : ∃ (L : Submodule ℝ (Fin n → ℝ)), ↑L = linealitySpace_fin C ∧ ∃ (W : Submodule ℝ (Fin n → ℝ)), IsCompl W L ∧ ∃ (π : (Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ), LinearMap.ker π = L ∧ LinearMap.range π = W ∧ (∀ w ∈ W, π w = w) ∧ ∀ l ∈ L, π l = 0

Helper for Theorem 19.1: split off lineality using a complementary projection.

theorem helperForTheorem_19_1_projection_preimage_image_eq_of_linealityKernel {n : ℕ} {C : Set (Fin n → ℝ)} (hc : Convex ℝ C) (hCne : C.Nonempty) {L W : Submodule ℝ (Fin n → ℝ)} (hWL : IsCompl W L) {π : (Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ} (hker : LinearMap.ker π = L) (hrange : LinearMap.range π = W) (hL : ↑L = linealitySpace_fin C) : have K := ⇑π '' C; C = ⇑π ⁻¹' K ∧ K ⊆ ↑W ∧ K.Nonempty

Helper for Theorem 19.1: lineality-kernel projection gives preimage/image decomposition.

theorem helperForTheorem_19_1_face_preimage_of_projection {n : ℕ} {C K F : Set (Fin n → ℝ)} (hc : Convex ℝ C) {π : (Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ} (hK : K = ⇑π '' C) (hCpre : C = ⇑π ⁻¹' K) (hF : IsFace K F) : IsFace C (C ∩ ⇑π ⁻¹' F)

Helper for Theorem 19.1: pull back faces along a projection.

theorem helperForTheorem_19_1_closed_finiteFaces_noLines_of_linealityProjection {n : ℕ} {C : Set (Fin n → ℝ)} (hc : Convex ℝ C) (hclosed : IsClosed C) (hfaces : {F : Set (Fin n → ℝ) | IsFace C F}.Finite) (hCne : C.Nonempty) {L W : Submodule ℝ (Fin n → ℝ)} (hWL : IsCompl W L) {π : (Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ} (hker : LinearMap.ker π = L) (hrange : LinearMap.range π = W) (hprojW : ∀ w ∈ W, π w = w) (hL : ↑L = linealitySpace_fin C) : have K := ⇑π '' C; IsClosed K ∧ {F : Set (Fin n → ℝ) | IsFace K F}.Finite ∧ ¬∃ (y : Fin n → ℝ), y ≠ 0 ∧ y ∈ -K.recessionCone ∩ K.recessionCone

Helper for Theorem 19.1: properties of the projection along lineality.

theorem helperForTheorem_19_1_mixedConvexHull_recedes {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} {d x : Fin n → ℝ} (hd : d ∈ S₁) (hx : x ∈ mixedConvexHull S₀ S₁) (t : ℝ) : 0 ≤ t → x + t • d ∈ mixedConvexHull S₀ S₁

Helper for Theorem 19.1: mixed convex hulls recede along their direction set.

theorem helperForTheorem_19_1_cone_mono {n : ℕ} {S T : Set (Fin n → ℝ)} (hST : S ⊆ T) : cone n S ⊆ cone n T

Helper for Theorem 19.1: monotonicity of the generated cone.

theorem helperForTheorem_19_1_recessionCone_subset_submodule {n : ℕ} {K : Set (Fin n → ℝ)} {W : Submodule ℝ (Fin n → ℝ)} (hKsubset : K ⊆ ↑W) (hKne : K.Nonempty) : K.recessionCone ⊆ ↑W

Helper for Theorem 19.1: recession directions of a subset of a submodule lie in it.

theorem helperForTheorem_19_1_submodule_subset_cone_of_finiteBasis {n : ℕ} (L : Submodule ℝ (Fin n → ℝ)) : ∃ (SL : Set (Fin n → ℝ)), SL.Finite ∧ SL ⊆ ↑L ∧ ↑L ⊆ cone n SL

Helper for Theorem 19.1: a finite basis yields a finite cone covering a submodule.