theorem coneSet_mem_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 at scale 1 is exactly membership in the base set.

theorem coneSet_intersection_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 := K1 ∩ K2; (1, x) ∈ K ↔ x ∈ C1 ∩ C2

Text 3.6.12: For sets C1 and C2, let K1 = { (λ, x) | 0 ≤ λ ∧ x ∈ λ • C1 }, K2 = { (λ, x) | 0 ≤ λ ∧ x ∈ λ • C2 }, and K = { (λ, x) | (λ, x) ∈ K1, (λ, x) ∈ K2 }. Then (1, x) ∈ K iff x ∈ C1 ∩ C2.

theorem convex_coneSet_intersection {n : ℕ} {C1 C2 : Set (Fin n → ℝ)} (hC1 : Convex ℝ C1) (hC2 : Convex ℝ C2) : 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 := K1 ∩ K2; Convex ℝ K

Text 3.6.13: For convex sets C1 and C2, let K1 = { (λ, x) | 0 ≤ λ ∧ x ∈ λ • C1 }, K2 = { (λ, x) | 0 ≤ λ ∧ x ∈ λ • C2 }, and K = { (λ, x) | (λ, x) ∈ K1, (λ, x) ∈ K2 }. Then K is convex.

theorem convex_H_hyperplane_one {n : ℕ} : Convex ℝ {p : ℝ × (Fin n → ℝ) | p.1 = 1}

The hyperplane {(1, x)} in ℝ × ℝ^n is convex.

theorem inverseAddition_eq_snd_image_K_inter_H {n : ℕ} {C1 C2 : Set (Fin n → ℝ)} (hC1 : Convex ℝ C1) (hC2 : Convex ℝ C2) : 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 → ℝ) | ∃ (r1 : ℝ) (r2 : ℝ), p.1 = r1 + r2 ∧ (r1, p.2) ∈ K1 ∧ (r2, p.2) ∈ K2}; have H := {p : ℝ × (Fin n → ℝ) | p.1 = 1}; (C1 # C2) = ⇑(LinearMap.snd ℝ ℝ (Fin n → ℝ)) '' (K ∩ H)

The inverse addition is the projection of K ∩ H to the second coordinate.

theorem convex_K_inter_H {n : ℕ} {C1 C2 : Set (Fin n → ℝ)} (hC1 : Convex ℝ C1) (hC2 : Convex ℝ C2) : 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 → ℝ) | ∃ (r1 : ℝ) (r2 : ℝ), p.1 = r1 + r2 ∧ (r1, p.2) ∈ K1 ∧ (r2, p.2) ∈ K2}; have H := {p : ℝ × (Fin n → ℝ) | p.1 = 1}; Convex ℝ (K ∩ H)

The intersection of the cone-set K with the hyperplane H is convex.

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

Theorem 3.7: If C1 and C2 are convex sets in ℝ^n, then their inverse sum C1 # C2 is convex.