theorem image_add_right_eq_image_add_left {n : ℕ} (C : Set (Fin n → ℝ)) (a : Fin n → ℝ) : (fun (x : Fin n → ℝ) => x + a) '' C = (fun (x : Fin n → ℝ) => a + x) '' C

Translation by adding on the right equals translation by adding on the left.

theorem convex_translate {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) (a : Fin n → ℝ) : Convex ℝ ((fun (x : Fin n → ℝ) => x + a) '' C)

Theorem 3.0.1: If C is a convex set in Real^n, then C + a is convex for any a in Real^n.

theorem convex_smul_image {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) (r : ℝ) : Convex ℝ ((fun (x : Fin n → ℝ) => r • x) '' C)

Theorem 3.0.2: If C is a convex set in Real^n, then r C = {r x | x ∈ C} is convex for any r ∈ Real.

theorem convex_add {n : ℕ} {C1 C2 : Set (Fin n → ℝ)} (hC1 : Convex ℝ C1) (hC2 : Convex ℝ C2) : Convex ℝ (C1 + C2)

Theorem 3.1: If C1 and C2 are convex sets in Real^n, then their sum C1 + C2 = {x1 + x2 | x1 ∈ C1, x2 ∈ C2} is convex.

theorem upper_set_subset_add_nonneg {n : ℕ} {C1 : Set (Fin n → ℝ)} : {x : Fin n → ℝ | ∃ x1 ∈ C1, x1 ≤ x} ⊆ C1 + Set.Ici 0

The upper set {x | ∃ x1 ∈ C1, x1 ≤ x} lies in C1 + {x | 0 ≤ x}.

theorem convex_nonneg_orthant {n : ℕ} : Convex ℝ (Set.Ici 0)

A pointwise nonnegative orthant is a convex set.

theorem add_nonneg_subset_upper_set {n : ℕ} {C1 : Set (Fin n → ℝ)} : C1 + Set.Ici 0 ⊆ {x : Fin n → ℝ | ∃ x1 ∈ C1, x1 ≤ x}

The sum with the nonnegative orthant lies in the upper set.

theorem convex_upper_set_of_le {n : ℕ} {C1 : Set (Fin n → ℝ)} (hC1 : Convex ℝ C1) : Convex ℝ {x : Fin n → ℝ | ∃ x1 ∈ C1, x1 ≤ x}

Text 3.1.1: If C1 is a convex set in R^n, then the set {x | ∃ x1 ∈ C1, x1 ≤ x} is also convex, where ≤ is understood componentwise.

theorem smul_mem_of_smul_subset {n : ℕ} {K : Set (Fin n → ℝ)} (hK : ∀ {r : ℝ}, 0 < r → r • K ⊆ K) {r : ℝ} (hr : 0 < r) {x : Fin n → ℝ} (hx : x ∈ K) : r • x ∈ K

Unpack the inclusion r • K ⊆ K into pointwise closure under scaling.

theorem add_mem_of_add_subset {n : ℕ} {K : Set (Fin n → ℝ)} (hK : K + K ⊆ K) {x y : Fin n → ℝ} (hx : x ∈ K) (hy : y ∈ K) : x + y ∈ K

Unpack the inclusion K + K ⊆ K into pointwise closure under addition.

theorem convexCone_iff_smul_subset_add_subset {n : ℕ} (K : Set (Fin n → ℝ)) : (∃ (C : ConvexCone ℝ (Fin n → ℝ)), ↑C = K) ↔ (∀ {r : ℝ}, 0 < r → r • K ⊆ K) ∧ K + K ⊆ K

Text 3.1.2: A set K is a convex cone iff for every λ > 0 we have λ • K ⊆ K, and K + K ⊆ K.

theorem convex_sum_finset_set {n : ℕ} {ι : Type u_1} (s : Finset ι) (A : ι → Set (Fin n → ℝ)) (hA : ∀ i ∈ s, Convex ℝ (A i)) : Convex ℝ (s.sum A)

A finite Minkowski sum of convex sets is convex.

theorem convex_linear_combination {n m : ℕ} (C : Fin m → Set (Fin n → ℝ)) (w : Fin m → ℝ) (hC : ∀ (i : Fin m), Convex ℝ (C i)) : Convex ℝ (∑ i : Fin m, w i • C i)

Text 3.1.3: If C1, ..., Cm are convex sets, then the linear combination C = lambda_1 • C1 + ... + lambda_m • Cm is convex.

def IsConvexCombinationSet {n m : ℕ} (C : Set (Fin n → ℝ)) (C' : Fin m → Set (Fin n → ℝ)) (w : Fin m → ℝ) : Prop

Text 3.1.4: A set C = lambda_1 • C1 + ... + lambda_m • Cm is called a convex combination of C1, ..., Cm when lambda_i ≥ 0 for all i and lambda_1 + ... + lambda_m = 1.

Equations

• IsConvexCombinationSet C C' w = (C = ∑ i : Fin m, w i • C' i ∧ (∀ (i : Fin m), 0 ≤ w i) ∧ ∑ i : Fin m, w i = 1)

theorem minkowski_sum_subset_iUnion_translate {n : ℕ} (C1 C2 : Set (Fin n → ℝ)) : C1 + C2 ⊆ ⋃ x1 ∈ C1, (fun (x2 : Fin n → ℝ) => x1 + x2) '' C2

A Minkowski sum point lies in a translate of the second set.

theorem iUnion_translate_subset_minkowski_sum {n : ℕ} (C1 C2 : Set (Fin n → ℝ)) : ⋃ x1 ∈ C1, (fun (x2 : Fin n → ℝ) => x1 + x2) '' C2 ⊆ C1 + C2

A point in a translate union lies in the Minkowski sum.

theorem minkowski_sum_eq_iUnion_translate {n : ℕ} (C1 C2 : Set (Fin n → ℝ)) : C1 + C2 = ⋃ x1 ∈ C1, (fun (x2 : Fin n → ℝ) => x1 + x2) '' C2

Text 3.1.5: For sets C1, C2 ⊆ ℝ^n, the Minkowski sum satisfies C1 + C2 = ⋃ x1 ∈ C1, (x1 + C2), where x1 + C2 = {x1 + x2 | x2 ∈ C2} is the translate of C2 by the vector x1.

theorem minkowski_sum_comm {n : ℕ} (C1 C2 : Set (Fin n → ℝ)) : C1 + C2 = C2 + C1

Minkowski sum is commutative.

theorem minkowski_sum_assoc {n : ℕ} (C1 C2 C3 : Set (Fin n → ℝ)) : C1 + C2 + C3 = C1 + (C2 + C3)

Minkowski sum is associative.

theorem smul_smul_set {n : ℕ} (C : Set (Fin n → ℝ)) (r1 r2 : ℝ) : r1 • r2 • C = (r1 * r2) • C

Scalar multiplication on sets is associative.

theorem smul_add_set {n : ℕ} (C1 C2 : Set (Fin n → ℝ)) (r : ℝ) : r • (C1 + C2) = r • C1 + r • C2

Scalar multiplication distributes over Minkowski sums.

theorem smul_set_subset_add_smul_set {n : ℕ} (C : Set (Fin n → ℝ)) (r1 r2 : ℝ) : (r1 + r2) • C ⊆ r1 • C + r2 • C

The easy inclusion of a scaled set into a Minkowski sum of scaled sets.

theorem convex_combo_subset {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : a • C + b • C ⊆ C

Convexity gives closure under binary convex combinations inside C.

theorem add_smul_subset_smul_of_pos {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) {r1 r2 : ℝ} (hr1 : 0 ≤ r1) (hr2 : 0 ≤ r2) (hpos : 0 < r1 + r2) : r1 • C + r2 • C ⊆ (r1 + r2) • C

Scale a convex combination back to a Minkowski sum of scaled sets.

theorem minkowski_sum_smul_properties {n : ℕ} (C1 C2 C3 C : Set (Fin n → ℝ)) (r1 r2 r : ℝ) : C1 + C2 = C2 + C1 ∧ C1 + C2 + C3 = C1 + (C2 + C3) ∧ r1 • r2 • C = (r1 * r2) • C ∧ r • (C1 + C2) = r • C1 + r • C2

Text 3.1.6: For sets C1, C2, C3 in ℝ^n and real numbers λ1, λ2, λ, the Minkowski sum is commutative and associative, scalar multiplication is associative, and scalar multiplication distributes over sums: C1 + C2 = C2 + C1, (C1 + C2) + C3 = C1 + (C2 + C3), λ1(λ2 C) = (λ1 λ2) C, and λ(C1 + C2) = λ C1 + λ C2.

theorem convex_smul_add_eq {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) {r1 r2 : ℝ} (hr1 : 0 ≤ r1) (hr2 : 0 ≤ r2) : (r1 + r2) • C = r1 • C + r2 • C

Theorem 3.2: If C is a convex set in Real^n and λ1 ≥ 0, λ2 ≥ 0, then (λ1 + λ2) • C = λ1 • C + λ2 • C.

theorem convex_eq_smul_add_smul_self {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r ≤ 1) : C = r • C + (1 - r) • C

Text 3.2.1: For a convex set C ⊆ ℝ^n and any λ with 1 ≥ λ ≥ 0, it holds that C = λ • C + (1 - λ) • C.

theorem convex_add_eq_two_smul {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) : C + C = 2 • C

Text 3.2.2: For a convex set C ⊆ ℝ^n, it holds that C + C = 2C.

theorem convex_add_eq_three_smul {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) : C + C + C = 3 • C

Text 3.2.3: For a convex set C ⊆ ℝ^n, it holds that C + C + C = 3C.

theorem mem_sum_smul_set_iff_exists_points {n m : ℕ} (C : Fin m → Set (Fin n → ℝ)) (w : Fin m → ℝ) (x : Fin n → ℝ) : x ∈ ∑ i : Fin m, w i • C i ↔ ∃ (z : Fin m → Fin n → ℝ), (∀ (i : Fin m), z i ∈ C i) ∧ x = ∑ i : Fin m, w i • z i

Membership in a finite Minkowski sum of scaled sets is equivalent to a pointwise witness.

theorem choose_index_family_of_mem_iUnion {n m : ℕ} {I : Type u_1} {C : I → Set (Fin n → ℝ)} {x : Fin m → Fin n → ℝ} (hx : ∀ (i : Fin m), x i ∈ ⋃ (j : I), C j) : ∃ (f : Fin m → I), ∀ (i : Fin m), x i ∈ C (f i)

Choose indices witnessing membership in a union of sets.

theorem convexHull_iUnion_eq_setOf_finite_convexCombinations {n : ℕ} {I : Type u_1} (C : I → Set (Fin n → ℝ)) (_hCne : ∀ (i : I), (C i).Nonempty) (_hCconv : ∀ (i : I), Convex ℝ (C i)) : (convexHull ℝ) (⋃ (i : I), C i) = {x : Fin n → ℝ | ∃ (m : ℕ) (f : Fin m → I) (w : Fin m → ℝ), (∀ (i : Fin m), 0 ≤ w i) ∧ ∑ i : Fin m, w i = 1 ∧ x ∈ ∑ i : Fin m, w i • C (f i)}

Theorem 3.3: If {C_i | i ∈ I} is a collection of nonempty convex sets in ℝ^n and C is the convex hull of their union, then C is the union of all finite convex combinations ∑ i, λ_i C_i, where the coefficients are nonnegative, only finitely many are nonzero, and they sum to 1.

def linearImage {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (C : Set (Fin n → ℝ)) : Set (Fin m → ℝ)

Text 3.4.0: Given a linear transformation A from ℝ^n to ℝ^m, the image of C ⊆ ℝ^n under A is AC = {A x | x ∈ C}.

Equations

• linearImage A C = ⇑A '' C

def linearPreimage {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (D : Set (Fin m → ℝ)) : Set (Fin n → ℝ)

Text 3.4.0: Given a linear transformation A from ℝ^n to ℝ^m, the inverse image of D ⊆ ℝ^m under A is A⁻¹ D = {x | A x ∈ D}.

Equations

• linearPreimage A D = ⇑A ⁻¹' D

theorem convex_linearImage {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) : Convex ℝ (linearImage A C)

Linear images of convex sets are convex.

theorem convex_linearPreimage {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) {D : Set (Fin m → ℝ)} (hD : Convex ℝ D) : Convex ℝ (linearPreimage A D)

Linear preimages of convex sets are convex.

theorem convex_linearImage_and_preimage {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) : (∀ {C : Set (Fin n → ℝ)}, Convex ℝ C → Convex ℝ (linearImage A C)) ∧ ∀ {D : Set (Fin m → ℝ)}, Convex ℝ D → Convex ℝ (linearPreimage A D)

Theorem 3.4: Let A be a linear transformation from ℝ^n to ℝ^m. Then A C is a convex set in ℝ^m for every convex set C in ℝ^n, and A⁻¹ D is a convex set in ℝ^n for every convex set D in ℝ^m.

theorem convex_orthogonalProjection {n : ℕ} (L : Submodule ℝ (EuclideanSpace ℝ (Fin n))) [L.HasOrthogonalProjection] {C : Set (EuclideanSpace ℝ (Fin n))} (hC : Convex ℝ C) : Convex ℝ (⇑L.starProjection '' C)

Corollary 3.4.1: The orthogonal projection of a convex set C on a subspace L is another convex set.

theorem translate_nonneg_orthant_eq_ge {m : ℕ} (a : Fin m → ℝ) : (fun (u : Fin m → ℝ) => u + a) '' {u : Fin m → ℝ | 0 ≤ u} = {y : Fin m → ℝ | y ≥ a}

Translating the nonnegative orthant yields the upper set ≥ a.

theorem linearPreimage_translate_nonneg_orthant_eq_ge {m n : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (a : Fin m → ℝ) : linearPreimage A ((fun (u : Fin m → ℝ) => u + a) '' {u : Fin m → ℝ | 0 ≤ u}) = {x : Fin n → ℝ | A x ≥ a}

The preimage of the translated nonnegative orthant is a pointwise inequality.

theorem linearImage_nonneg_orthant_eq_exists {m n : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) : linearImage A {x : Fin n → ℝ | 0 ≤ x} = {y : Fin m → ℝ | ∃ (x : Fin n → ℝ), 0 ≤ x ∧ A x = y}

The image of the nonnegative orthant is characterized by existence.

theorem linearImage_preimage_nonneg_orthant {m n : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (a : Fin m → ℝ) : have K := {u : Fin m → ℝ | 0 ≤ u}; have C := {x : Fin n → ℝ | 0 ≤ x}; have D := (fun (u : Fin m → ℝ) => u + a) '' K; D = {y : Fin m → ℝ | y ≥ a} ∧ linearPreimage A D = {x : Fin n → ℝ | A x ≥ a} ∧ linearImage A C = {y : Fin m → ℝ | ∃ (x : Fin n → ℝ), 0 ≤ x ∧ A x = y}

Text 3.4.2: Let A ∈ ℝ^{m×n}. Define the nonnegative orthants K = {u ∈ ℝ^m | u ≥ 0} and C = {x ∈ ℝ^n | x ≥ 0} and for a ∈ ℝ^m set D = K + a = {u + a | u ∈ K} = {y ∈ ℝ^m | y ≥ a}. Then the preimage A⁻¹ D equals {x ∈ ℝ^n | A x ≥ a} and the image A C equals {y ∈ ℝ^m | ∃ x ∈ ℝ^n_+, A x = y}.

theorem convex_prod {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} (hC : Convex ℝ C) (hD : Convex ℝ D) : Convex ℝ (C.prod D)

Theorem 3.5: For convex sets C ⊆ ℝ^m and D ⊆ ℝ^n, the direct-sum set C ⊕ D = {x = (y, z) | y ∈ C, z ∈ D} is a convex set in ℝ^{m+n}.

def directSumSet {m n : ℕ} (C : Set (Fin m → ℝ)) (D : Set (Fin n → ℝ)) : Set ((Fin m → ℝ) × (Fin n → ℝ))

Text 3.5.1: Let C and D be convex sets in ℝ^m and ℝ^n. Then C ⊕ D = {x = (y, z) | y ∈ C, z ∈ D} is called the direct sum of C and D.

Equations

• directSumSet C D = C.prod D

theorem convex_directSumSet {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} (hC : Convex ℝ C) (hD : Convex ℝ D) : Convex ℝ (directSumSet C D)

Text 3.5.2: The direct sum of two convex sets is convex.

theorem unique_decomp_imp_intersection_subset_zero {n : ℕ} {C D : Set (Fin n → ℝ)} (huniq : ∀ x ∈ C + D, ∃! yz : (Fin n → ℝ) × (Fin n → ℝ), yz.1 ∈ C ∧ yz.2 ∈ D ∧ x = yz.1 + yz.2) (v : Fin n → ℝ) : v ∈ (C - C) ∩ (D - D) → v = 0

Unique decomposition forces elements of (C - C) ∩ (D - D) to be zero.

theorem zero_mem_intersection_of_nonempty {n : ℕ} {C D : Set (Fin n → ℝ)} (hC : C.Nonempty) (hD : D.Nonempty) : 0 ∈ (C - C) ∩ (D - D)

If C and D are nonempty, then 0 ∈ (C - C) ∩ (D - D).

theorem intersection_eq_zero_imp_unique_decomp {n : ℕ} {C D : Set (Fin n → ℝ)} (hinter : (C - C) ∩ (D - D) = {0}) (x : Fin n → ℝ) : x ∈ C + D → ∃! yz : (Fin n → ℝ) × (Fin n → ℝ), yz.1 ∈ C ∧ yz.2 ∈ D ∧ x = yz.1 + yz.2

Intersection criterion implies uniqueness of decompositions in C + D.

theorem unique_decomposition_iff_intersection_sub {n : ℕ} (C D : Set (Fin n → ℝ)) (hC : C.Nonempty) (hD : D.Nonempty) : (∀ x ∈ C + D, ∃! yz : (Fin n → ℝ) × (Fin n → ℝ), yz.1 ∈ C ∧ yz.2 ∈ D ∧ x = yz.1 + yz.2) ↔ (C - C) ∩ (D - D) = {0}

Text 3.5.3: For sets C, D ⊆ ℝ^n, the following are equivalent: (1) (Unique decomposition) Every x ∈ C + D can be written in a unique way as x = y + z with (y, z) ∈ C × D. (2) (Intersection criterion) (C - C) ∩ (D - D) = {0}.

theorem convex_sub_self {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) : Convex ℝ (C - C)

Text 3.5.4: If C ⊆ ℝ^n is convex, then C - C is a convex set.

theorem coneSet_smul_mem {n : ℕ} {C : Set (Fin n → ℝ)} {r a : ℝ} {x : Fin n → ℝ} (hx : x ∈ r • C) : a • x ∈ (a * r) • C

Push a scalar factor through membership in a scaled set.

theorem coneSet_combo_mem {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) {r1 r2 a b : ℝ} {x1 x2 : Fin n → ℝ} (hr1 : 0 ≤ r1) (hr2 : 0 ≤ r2) (hx1 : x1 ∈ r1 • C) (hx2 : x2 ∈ r2 • C) (ha : 0 ≤ a) (hb : 0 ≤ b) : a • x1 + b • x2 ∈ (a * r1 + b * r2) • C

Convexity combines elements of scaled sets into a larger scaled set.

theorem convex_coneSet_of_convex {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) : Convex ℝ {p : ℝ × (Fin n → ℝ) | 0 ≤ p.1 ∧ p.2 ∈ p.1 • C}

Text 3.5.5: For a convex set C ⊆ ℝ^n, the set K_C = { (λ, x) ∈ ℝ × ℝ^n | λ ≥ 0, x ∈ λ C } is convex.

theorem smul_add_smul_add_eq {p : ℕ} {a b : ℝ} (z1 z1' z2 z2' : Fin p → ℝ) : a • z1 + b • z1' + (a • z2 + b • z2') = a • (z1 + z2) + b • (z1' + z2')

Linear combinations distribute over coordinatewise additions in ℝ^p.

theorem convex_fiberwise_add {m p : ℕ} {C1 C2 : Set ((Fin m → ℝ) × (Fin p → ℝ))} (hC1 : Convex ℝ C1) (hC2 : Convex ℝ C2) : Convex ℝ {x : (Fin m → ℝ) × (Fin p → ℝ) | ∃ (z1 : Fin p → ℝ) (z2 : Fin p → ℝ), (x.1, z1) ∈ C1 ∧ (x.1, z2) ∈ C2 ∧ z1 + z2 = x.2}

Theorem 3.6: Let C1 and C2 be convex sets in ℝ^{m+p}. Let C be the set of vectors x = (y, z) with y ∈ ℝ^m and z ∈ ℝ^p such that there exist z1 and z2 with (y, z1) ∈ C1, (y, z2) ∈ C2, and z1 + z2 = z. Then C is a convex set in ℝ^{m+p}.

def inverseAddition {n : ℕ} (C1 C2 : Set (Fin n → ℝ)) : Set (Fin n → ℝ)

Text 3.6.1: Define the inverse addition C1 # C2 by ⋃₀ {S | ∃ λ1 λ2, 0 ≤ λ1, 0 ≤ λ2, λ1 + λ2 = 1, S = (λ1 • C1) ∩ (λ2 • C2)}, equivalently as ⋃₀ { (1 - λ) • C1 ∩ λ • C2 | 0 ≤ λ ∧ λ ≤ 1 }.

Equations

• (C1 # C2) = ⋃₀ {S : Set (Fin n → ℝ) | ∃ (r1 : ℝ) (r2 : ℝ), 0 ≤ r1 ∧ 0 ≤ r2 ∧ r1 + r2 = 1 ∧ S = r1 • C1 ∩ r2 • C2}

def «term_#_» : Lean.TrailingParserDescr

Equations

• «term_#_» = Lean.ParserDescr.trailingNode `«term_#_» 70 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " # ") (Lean.ParserDescr.cat `term 0))

theorem convex_fiberwise_add_left {m p : ℕ} {C1 C2 : Set ((Fin m → ℝ) × (Fin p → ℝ))} (hC1 : Convex ℝ C1) (hC2 : Convex ℝ C2) : Convex ℝ {x : (Fin m → ℝ) × (Fin p → ℝ) | ∃ (y1 : Fin m → ℝ) (y2 : Fin m → ℝ), (y1, x.2) ∈ C1 ∧ (y2, x.2) ∈ C2 ∧ y1 + y2 = x.1}

Text 3.6.2: Let C1 and C2 be convex sets in ℝ^{m+p}. Let C be the set of vectors x = (y, z) with y ∈ ℝ^m and z ∈ ℝ^p such that there exist y1 and y2 with (y1, z) ∈ C1, (y2, z) ∈ C2, and y1 + y2 = y. Then C is a convex set in ℝ^{m+p}.

theorem mem_add_prod_iff {m p : ℕ} {C1 C2 : Set ((Fin m → ℝ) × (Fin p → ℝ))} {x : (Fin m → ℝ) × (Fin p → ℝ)} : x ∈ {x : (Fin m → ℝ) × (Fin p → ℝ) | ∃ (y1 : Fin m → ℝ) (y2 : Fin m → ℝ) (z1 : Fin p → ℝ) (z2 : Fin p → ℝ), (y1, z1) ∈ C1 ∧ (y2, z2) ∈ C2 ∧ y1 + y2 = x.1 ∧ z1 + z2 = x.2} ↔ x ∈ C1 + C2

Membership in the componentwise-sum set is equivalent to membership in the Minkowski sum in the product space.

theorem convex_add_prod {m p : ℕ} {C1 C2 : Set ((Fin m → ℝ) × (Fin p → ℝ))} (hC1 : Convex ℝ C1) (hC2 : Convex ℝ C2) : Convex ℝ {x : (Fin m → ℝ) × (Fin p → ℝ) | ∃ (y1 : Fin m → ℝ) (y2 : Fin m → ℝ) (z1 : Fin p → ℝ) (z2 : Fin p → ℝ), (y1, z1) ∈ C1 ∧ (y2, z2) ∈ C2 ∧ y1 + y2 = x.1 ∧ z1 + z2 = x.2}

theorem convex_intersection {n : ℕ} {C1 C2 : Set (Fin n → ℝ)} (hC1 : Convex ℝ C1) (hC2 : Convex ℝ C2) : Convex ℝ (C1 ∩ C2)

Text 3.6.4: If C1 and C2 are convex sets in ℝ^n, then C1 ∩ C2 is convex.

theorem convex_intersection_prod {m p : ℕ} {C1 C2 : Set ((Fin m → ℝ) × (Fin p → ℝ))} (hC1 : Convex ℝ C1) (hC2 : Convex ℝ C2) : Convex ℝ (C1 ∩ C2)

Text 3.6.5: Let C1 and C2 be convex sets in ℝ^{m+p}. Let C be the set of vectors x = (y, z) with y ∈ ℝ^m and z ∈ ℝ^p such that (y, z) ∈ C1 and (y, z) ∈ C2. Then C is a convex set in ℝ^{m+p}.

theorem mem_coneSet_one_iff {n : ℕ} {C : Set (Fin n → ℝ)} {x : Fin n → ℝ} : (1, x) ∈ {p : ℝ × (Fin n → ℝ) | 0 ≤ p.1 ∧ p.2 ∈ p.1 • C} ↔ x ∈ C

Membership in the cone set at λ = 1 reduces to membership in the base set.

theorem mem_K_iff_exists_add {n : ℕ} {C1 C2 : Set (Fin n → ℝ)} {x : Fin n → ℝ} : (have K1 := {p : ℝ × (Fin n → ℝ) | 0 ≤ p.1 ∧ p.2 ∈ p.1 • C1}; have K2 := {p : ℝ × (Fin n → ℝ) | 0 ≤ p.1 ∧ p.2 ∈ p.1 • C2}; have K := {p : ℝ × (Fin n → ℝ) | ∃ (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), p.2 = x1 + x2 ∧ (p.1, x1) ∈ K1 ∧ (p.1, x2) ∈ K2}; (1, x) ∈ K) ↔ ∃ (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), x = x1 + x2 ∧ x1 ∈ C1 ∧ x2 ∈ C2

Unfolding the cone sum at λ = 1 yields a decomposition into C1 and C2.

theorem coneSet_add_iff {n : ℕ} {C1 C2 : Set (Fin n → ℝ)} (x : Fin n → ℝ) : have K1 := {p : ℝ × (Fin n → ℝ) | 0 ≤ p.1 ∧ p.2 ∈ p.1 • C1}; have K2 := {p : ℝ × (Fin n → ℝ) | 0 ≤ p.1 ∧ p.2 ∈ p.1 • C2}; have K := {p : ℝ × (Fin n → ℝ) | ∃ (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), p.2 = x1 + x2 ∧ (p.1, x1) ∈ K1 ∧ (p.1, x2) ∈ K2}; (1, x) ∈ K ↔ x ∈ C1 + C2

Text 3.6.6: For convex sets C1 and C2 in ℝ^n, define K1 = { (λ, x) | 0 ≤ λ ∧ x ∈ λ • C1 }, K2 = { (λ, x) | 0 ≤ λ ∧ x ∈ λ • C2 }, and K = { (λ, x) | ∃ x1 x2, x = x1 + x2 ∧ (λ, x1) ∈ K1 ∧ (λ, x2) ∈ K2 }. Then (1, x) ∈ K iff x ∈ C1 + C2.