theorem isPolyhedralConvexSet_iff_exists_finite_halfspaces (n : ℕ) (C : Set (Fin n → ℝ)) : IsPolyhedralConvexSet n C ↔ ∃ (m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ), C = ⋂ (i : Fin m), closedHalfSpaceLE n (b i) (β i)

Text 19.0.1: A set C ⊆ ℝ^n is polyhedral convex if there exist vectors b i and scalars β i such that C is the intersection of finitely many closed half-spaces {x | x ⬝ᵥ b i ≤ β i}.

theorem helperForText_19_0_2_eq_iff_le_and_neg_le {n : ℕ} {x a : Fin n → ℝ} {α : ℝ} : x ⬝ᵥ a = α ↔ x ⬝ᵥ a ≤ α ∧ x ⬝ᵥ -a ≤ -α

Helper for Text 19.0.2: an equality is equivalent to two weak inequalities.

theorem helperForText_19_0_2_solutionSet_as_iInter_halfspaces (n m k : ℕ) (a : Fin m → Fin n → ℝ) (α : Fin m → ℝ) (b : Fin k → Fin n → ℝ) (β : Fin k → ℝ) : {x : Fin n → ℝ | (∀ (i : Fin m), x ⬝ᵥ a i = α i) ∧ ∀ (j : Fin k), x ⬝ᵥ b j ≤ β j} = ⋂ (s : Fin m ⊕ Fin m ⊕ Fin k), closedHalfSpaceLE n (match (motive := Fin m ⊕ Fin m ⊕ Fin k → Fin n → ℝ) s with | Sum.inl i => a i | Sum.inr s' => match (motive := Fin m ⊕ Fin k → Fin n → ℝ) s' with | Sum.inl i => -a i | Sum.inr j => b j) (match s with | Sum.inl i => α i | Sum.inr s' => match s' with | Sum.inl i => -α i | Sum.inr j => β j)

Helper for Text 19.0.2: rewrite the mixed system as a finite intersection of half-spaces.

theorem polyhedralConvexSet_solutionSet_linearEq_and_inequalities (n m k : ℕ) (a : Fin m → Fin n → ℝ) (α : Fin m → ℝ) (b : Fin k → Fin n → ℝ) (β : Fin k → ℝ) : IsPolyhedralConvexSet n {x : Fin n → ℝ | (∀ (i : Fin m), x ⬝ᵥ a i = α i) ∧ ∀ (j : Fin k), x ⬝ᵥ b j ≤ β j}

Text 19.0.2: The solution set in ℝ^n of any finite mixed system of linear equations and weak linear inequalities is a polyhedral convex set.

theorem helperForText_19_0_3_isCone_iInter_halfspaces_zero (n m : ℕ) (b : Fin m → Fin n → ℝ) : IsConeSet n (⋂ (i : Fin m), closedHalfSpaceLE n (b i) 0)

Helper for Text 19.0.3: intersections of homogeneous closed half-spaces are cones.

theorem helperForText_19_0_3_dot_le_zero_of_cone_and_mem_iInter {n : ℕ} {ι : Sort u_1} {C : Set (Fin n → ℝ)} {b : ι → Fin n → ℝ} {β : ι → ℝ} (hC : C = ⋂ (i : ι), closedHalfSpaceLE n (b i) (β i)) (hcone : IsConeSet n C) (x : Fin n → ℝ) : x ∈ C → ∀ (i : ι), x ⬝ᵥ b i ≤ 0

Helper for Text 19.0.3: a cone inside half-spaces forces each dot-product to be nonpositive.

theorem helperForText_19_0_3_beta_nonneg_of_cone_and_mem_iInter {n : ℕ} {ι : Sort u_1} {C : Set (Fin n → ℝ)} {b : ι → Fin n → ℝ} {β : ι → ℝ} (hC : C = ⋂ (i : ι), closedHalfSpaceLE n (b i) (β i)) (hCne : C.Nonempty) (hcone : IsConeSet n C) (i : ι) : 0 ≤ β i

Helper for Text 19.0.3: a nonempty cone inside half-spaces forces each β i to be nonnegative.

theorem helperForText_19_0_3_homogenize_iInter_halfspaces {n : ℕ} {ι : Sort u_1} {C : Set (Fin n → ℝ)} {b : ι → Fin n → ℝ} {β : ι → ℝ} (hC : C = ⋂ (i : ι), closedHalfSpaceLE n (b i) (β i)) (hCne : C.Nonempty) (hcone : IsConeSet n C) : C = ⋂ (i : ι), closedHalfSpaceLE n (b i) 0

Helper for Text 19.0.3: homogenize a half-space representation of a nonempty cone.

theorem polyhedralConvexSet_isCone_iff_iInter_halfspaces_through_origin (n : ℕ) (C : Set (Fin n → ℝ)) (hCne : C.Nonempty) : IsPolyhedralConvexSet n C → (IsConeSet n C ↔ ∃ (m : ℕ) (b : Fin m → Fin n → ℝ), C = ⋂ (i : Fin m), closedHalfSpaceLE n (b i) 0)

Text 19.0.3: For a polyhedral convex set C ⊆ ℝ^n, C is a cone iff it is the intersection of finitely many closed half-spaces whose boundary hyperplanes pass through the origin (equivalently, the inequalities are homogeneous with β i = 0).

def IsFinitelyGeneratedConvexSet (n : ℕ) (C : Set (Fin n → ℝ)) : Prop

Text 19.0.4: A convex set C ⊆ ℝ^n is called finitely generated if it is the mixed convex hull of finitely many points and directions (Definition 17.0.4). Equivalently, there exist vectors a₁, …, a_m and an integer k with 0 ≤ k ≤ m such that C consists exactly of all vectors of the form x = λ₁ a₁ + ··· + λ_m a_m with λ₁ + ··· + λ_k = 1 and λ_i ≥ 0 for i = 1, …, m.

Equations

• IsFinitelyGeneratedConvexSet n C = ∃ (S₀ : Set (Fin n → ℝ)) (S₁ : Set (Fin n → ℝ)), S₀.Finite ∧ S₁.Finite ∧ C = mixedConvexHull S₀ S₁

def IsGeneratingSetForConvexCone (n m : ℕ) (C : Set (Fin n → ℝ)) (a : Fin m → Fin n → ℝ) : Prop

Text 19.0.5: Let C ⊆ ℝ^n be a finitely generated convex cone. A finite set {a₁, …, a_m} is called a set of generators of C if C = {∑ i, λ i • a i | λ i ≥ 0} (equivalently, C = convexConeGenerated n (Set.range a)).

Equations

• IsGeneratingSetForConvexCone n m C a = (C = {x : Fin n → ℝ | ∃ (lam : Fin m → ℝ), (∀ (i : Fin m), 0 ≤ lam i) ∧ x = ∑ i : Fin m, lam i • a i})

def IsGeneralizedPolytopeWithVerticesAtInfinity (n : ℕ) (C : Set (Fin n → ℝ)) : Prop

Text 19.0.6: The unbounded finitely generated convex sets may be regarded as generalized polytopes having certain vertices at infinity, like the generalized simplices in §17.

Equations

• IsGeneralizedPolytopeWithVerticesAtInfinity n C = (IsFinitelyGeneratedConvexSet n C ∧ ¬Bornology.IsBounded C)

theorem helperForText_19_0_7_face_subset {n : ℕ} {C F : Set (Fin n → ℝ)} : IsFace C F → F ⊆ C

Helper for Text 19.0.7: a face is a subset of its ambient set.

theorem helperForText_19_0_7_face_convex {n : ℕ} {C F : Set (Fin n → ℝ)} : IsFace C F → Convex ℝ C

Helper for Text 19.0.7: a face certifies convexity of the ambient set.

theorem helperForText_19_0_7_face_isExtreme {n : ℕ} {C F : Set (Fin n → ℝ)} : IsFace C F → IsExtreme ℝ C F

Helper for Text 19.0.7: a face is an extreme subset of the ambient set.

theorem helperForText_19_0_7_polyhedral_isConvex (n : ℕ) (C : Set (Fin n → ℝ)) : IsPolyhedralConvexSet n C → Convex ℝ C

Helper for Text 19.0.7: polyhedral convex sets are convex.

theorem helperForText_19_0_7_polyhedral_empty (n : ℕ) : IsPolyhedralConvexSet n ∅

Helper for Text 19.0.7: the empty set is polyhedral convex.

theorem helperForText_19_0_7_exists_mem_euclideanRelativeInterior_fin_of_convex_nonempty {n : ℕ} {F : Set (Fin n → ℝ)} (hconvF : Convex ℝ F) (hFne : F.Nonempty) : ∃ (z : Fin n → ℝ), z ∈ euclideanRelativeInterior_fin n F

Helper for Text 19.0.7: a nonempty convex set in Fin n → ℝ has a relative interior point.

theorem helperForText_19_0_7_activeConstraintIntersection_isPolyhedral {n m : ℕ} (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ) (A : Set (Fin m)) : IsPolyhedralConvexSet n ((⋂ (j : Fin m), closedHalfSpaceLE n (b j) (β j)) ∩ ⋂ i ∈ A, {x : Fin n → ℝ | x ⬝ᵥ b i = β i})

Helper for Text 19.0.7: adding finitely many equality constraints to a finite half-space representation preserves polyhedrality.

theorem helperForTheorem_19_1_polyhedral_isConvex (n : ℕ) (C : Set (Fin n → ℝ)) : IsPolyhedralConvexSet n C → Convex ℝ C

Helper for Theorem 19.1: polyhedral convex sets are convex.

theorem helperForTheorem_19_1_polyhedral_isClosed (n : ℕ) (C : Set (Fin n → ℝ)) : IsPolyhedralConvexSet n C → IsClosed C

Helper for Theorem 19.1: polyhedral convex sets are closed.

theorem helperForTheorem_19_1_faces_as_IsExtreme_under_convex {n : ℕ} {C : Set (Fin n → ℝ)} (hc : Convex ℝ C) : {C' : Set (Fin n → ℝ) | IsFace C C'} = {C' : Set (Fin n → ℝ) | IsExtreme ℝ C C'}

Helper for Theorem 19.1: for convex sets, faces coincide with extreme subsets.

theorem helperForTheorem_19_1_faces_empty_of_not_convex {n : ℕ} {C : Set (Fin n → ℝ)} (hconv : ¬Convex ℝ C) : {C' : Set (Fin n → ℝ) | IsFace C C'} = ∅

Helper for Theorem 19.1: without convexity the family of faces is empty.

theorem helperForTheorem_19_1_closed_nonconvex_faces_finite : ∃ (C : Set (Fin 1 → ℝ)), IsClosed C ∧ {C' : Set (Fin 1 → ℝ) | IsFace C C'}.Finite ∧ ¬IsPolyhedralConvexSet 1 C

Helper for Theorem 19.1: a closed nonconvex set has finitely many faces.

theorem helperForTheorem_19_1_counterexample_equiv_false : ∃ (C : Set (Fin 1 → ℝ)), IsClosed C ∧ {C' : Set (Fin 1 → ℝ) | IsFace C C'}.Finite ∧ ¬(IsPolyhedralConvexSet 1 C ↔ IsClosed C ∧ {C' : Set (Fin 1 → ℝ) | IsFace C C'}.Finite)

Helper for Theorem 19.1: the stated equivalence fails without convexity.

theorem helperForTheorem_19_1_isFace_of_tightConstraint {n : ℕ} {C : Set (Fin n → ℝ)} {b : Fin n → ℝ} {β : ℝ} (hC : C ⊆ closedHalfSpaceLE n b β) (hc : Convex ℝ C) : IsFace C (C ∩ {x : Fin n → ℝ | x ⬝ᵥ b = β})

Helper for Theorem 19.1: a tight constraint defines a face of a convex set.

theorem helperForTheorem_19_1_face_subset_iInter_tightConstraints_of_mem_ri {n : ℕ} {ι : Type u_1} [Fintype ι] {C F : Set (Fin n → ℝ)} (b : ι → Fin n → ℝ) (β : ι → ℝ) (hC : C = ⋂ (i : ι), closedHalfSpaceLE n (b i) (β i)) (hF : IsFace C F) {z : Fin n → ℝ} (hzri : z ∈ euclideanRelativeInterior_fin n F) (hzC : z ∈ C) : F ⊆ C ∩ ⋂ i ∈ {i : ι | z ⬝ᵥ b i = β i}, {x : Fin n → ℝ | x ⬝ᵥ b i = β i}

Helper for Theorem 19.1: a face lies in all tight constraints at a relative interior point.

theorem helperForTheorem_19_1_mem_of_euclideanRelativeInterior_fin {n : ℕ} {C : Set (Fin n → ℝ)} {x : Fin n → ℝ} (hx : x ∈ euclideanRelativeInterior_fin n C) : x ∈ C

Helper for Theorem 19.1: a relative-interior point lies in the set.

theorem helperForTheorem_19_1_mem_euclideanRelativeInterior_fin_activeConstraintIntersection_of_mem {n : ℕ} {ι : Type u_1} [Fintype ι] {C : Set (Fin n → ℝ)} (b : ι → Fin n → ℝ) (β : ι → ℝ) (hC : C = ⋂ (i : ι), closedHalfSpaceLE n (b i) (β i)) {z : Fin n → ℝ} (hzC : z ∈ C) : z ∈ euclideanRelativeInterior_fin n (C ∩ ⋂ i ∈ {i : ι | z ⬝ᵥ b i = β i}, {x : Fin n → ℝ | x ⬝ᵥ b i = β i})

Helper for Theorem 19.1: an active-constraint intersection has a relative-interior point whenever the base point lies in the set.

theorem helperForTheorem_19_1_mem_euclideanRelativeInterior_fin_activeConstraintIntersection {n : ℕ} {ι : Type u_1} [Fintype ι] {C F : Set (Fin n → ℝ)} (b : ι → Fin n → ℝ) (β : ι → ℝ) (hC : C = ⋂ (i : ι), closedHalfSpaceLE n (b i) (β i)) (hF : IsFace C F) {z : Fin n → ℝ} (hzri : z ∈ euclideanRelativeInterior_fin n F) (hzC : z ∈ C) : z ∈ euclideanRelativeInterior_fin n (C ∩ ⋂ i ∈ {i : ι | z ⬝ᵥ b i = β i}, {x : Fin n → ℝ | x ⬝ᵥ b i = β i})

Helper for Theorem 19.1: the active-constraint intersection has the given relative interior point.

theorem helperForTheorem_19_1_face_eq_iInter_tightConstraints_of_mem_ri {n : ℕ} {ι : Type u_1} [Fintype ι] {C F : Set (Fin n → ℝ)} (b : ι → Fin n → ℝ) (β : ι → ℝ) (hC : C = ⋂ (i : ι), closedHalfSpaceLE n (b i) (β i)) (hF : IsFace C F) {z : Fin n → ℝ} (hzri : z ∈ euclideanRelativeInterior_fin n F) (hzC : z ∈ C) : C ∩ ⋂ i ∈ {i : ι | z ⬝ᵥ b i = β i}, {x : Fin n → ℝ | x ⬝ᵥ b i = β i} ⊆ F

Helper for Theorem 19.1: a face equals the intersection of its tight constraints at a relative-interior point.

theorem polyhedralConvexSet_face (n : ℕ) (C F : Set (Fin n → ℝ)) : IsPolyhedralConvexSet n C → IsFace C F → Convex ℝ F → IsPolyhedralConvexSet n F

Text 19.0.7: Every face of a polyhedral convex set is itself a polyhedral convex set.

theorem helperForTheorem_19_1_faces_finite_of_iInter_halfspaces {n : ℕ} {ι : Type u_1} [Fintype ι] {C : Set (Fin n → ℝ)} (b : ι → Fin n → ℝ) (β : ι → ℝ) (hC : C = ⋂ (i : ι), closedHalfSpaceLE n (b i) (β i)) : {F : Set (Fin n → ℝ) | IsFace C F}.Finite

Helper for Theorem 19.1: faces of a finite intersection of half-spaces are finite.

theorem helperForTheorem_19_1_polyhedral_imp_closed_finiteFaces {n : ℕ} {C : Set (Fin n → ℝ)} : IsPolyhedralConvexSet n C → IsClosed C ∧ {C' : Set (Fin n → ℝ) | IsFace C C'}.Finite

Helper for Theorem 19.1: polyhedral convex sets are closed and have finitely many faces.

theorem helperForTheorem_19_1_finiteFaces_imp_finite_extremePoints {n : ℕ} {C : Set (Fin n → ℝ)} (hc : Convex ℝ C) : {F : Set (Fin n → ℝ) | IsFace C F}.Finite → {x : Fin n → ℝ | IsExtremePoint C x}.Finite

Helper for Theorem 19.1: finite faces yield finitely many extreme points.