theorem convex_fiberwise_add_real {n : ℕ} {K1 K2 : Set (ℝ × (Fin n → ℝ))} (hK1 : Convex ℝ K1) (hK2 : Convex ℝ K2) : Convex ℝ {p : ℝ × (Fin n → ℝ) | ∃ (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), p.2 = x1 + x2 ∧ (p.1, x1) ∈ K1 ∧ (p.1, x2) ∈ K2}

Fiberwise addition over a real scalar coordinate preserves convexity.

theorem convex_fiberwise_add_real_left {n : ℕ} {K1 K2 : Set (ℝ × (Fin n → ℝ))} (hK1 : Convex ℝ K1) (hK2 : Convex ℝ K2) : Convex ℝ {p : ℝ × (Fin n → ℝ) | ∃ (r1 : ℝ) (r2 : ℝ), p.1 = r1 + r2 ∧ (r1, p.2) ∈ K1 ∧ (r2, p.2) ∈ K2}

Fiberwise addition on the real coordinate preserves convexity.

theorem convex_coneSet_add {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 → ℝ) | ∃ (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), p.2 = x1 + x2 ∧ (p.1, x1) ∈ K1 ∧ (p.1, x2) ∈ K2}; Convex ℝ K

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

theorem coneSet_inverseAddition_iff {n : ℕ} {C1 C2 : Set (Fin n → ℝ)} (_hC1 : Convex ℝ C1) (_hC2 : Convex ℝ C2) (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 → ℝ) | ∃ (r1 : ℝ) (r2 : ℝ), p.1 = r1 + r2 ∧ (r1, p.2) ∈ K1 ∧ (r2, p.2) ∈ K2}; (1, x) ∈ K ↔ x ∈ C1 # C2

Text 3.6.8: For convex sets C1 and C2, let K1 = { (λ, x) | 0 ≤ λ ∧ x ∈ λ • C1 }, K2 = { (λ, x) | 0 ≤ λ ∧ x ∈ λ • C2 }, and K = { (λ, x) | ∃ λ1 λ2, λ = λ1 + λ2, (λ1, x) ∈ K1, (λ2, x) ∈ K2 }. Then (1, x) ∈ K iff x ∈ C1 # C2.

theorem convex_coneSet_inverseAddition {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}; Convex ℝ K

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