theorem euclideanRelativeInterior_directSumSetEuclidean_superset (m p : ℕ) (C1 : Set (EuclideanSpace ℝ (Fin m))) (C2 : Set (EuclideanSpace ℝ (Fin p))) : directSumSetEuclidean m p (euclideanRelativeInterior m C1) (euclideanRelativeInterior p C2) ⊆ euclideanRelativeInterior (m + p) (directSumSetEuclidean m p C1 C2)

Reverse inclusion for the relative interior of a direct sum.

theorem euclideanRelativeInterior_directSumSetEuclidean_eq_and_closure_eq (m p : ℕ) (C1 : Set (EuclideanSpace ℝ (Fin m))) (C2 : Set (EuclideanSpace ℝ (Fin p))) : euclideanRelativeInterior (m + p) (directSumSetEuclidean m p C1 C2) = directSumSetEuclidean m p (euclideanRelativeInterior m C1) (euclideanRelativeInterior p C2) ∧ closure (directSumSetEuclidean m p C1 C2) = directSumSetEuclidean m p (closure C1) (closure C2)

Text 6.18: For the direct sum C1 ⊕ C2 in R^{m+p} of convex sets C1 ⊆ R^m and C2 ⊆ R^p (modeled as directSumSetEuclidean m p C1 C2), one has ri (C1 ⊕ C2) = ri C1 ⊕ ri C2 and cl (C1 ⊕ C2) = cl C1 ⊕ cl C2.

theorem mem_affineSpan_of_mem_closure {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} {y : EuclideanSpace ℝ (Fin n)} (hy : y ∈ closure C) : y ∈ ↑(affineSpan ℝ C)

Points in the closure lie in the affine span.

theorem norm_le_of_mem_smul_unitBall {n : ℕ} {ε : ℝ} (hε : 0 ≤ ε) {v : EuclideanSpace ℝ (Fin n)} (hv : v ∈ ε • euclideanUnitBall n) : ‖v‖ ≤ ε

A point in a scaled unit ball has norm bounded by the scale.

theorem mem_smul_unitBall_of_norm_le {n : ℕ} {ε : ℝ} (hε : 0 < ε) {v : EuclideanSpace ℝ (Fin n)} (hv : ‖v‖ ≤ ε) : v ∈ ε • euclideanUnitBall n

If a point has norm at most ε, it lies in the scaled unit ball ε • B.

theorem euclideanRelativeInterior_convex_combination_mem (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (x y : EuclideanSpace ℝ (Fin n)) (hx : x ∈ euclideanRelativeInterior n C) (hy : y ∈ closure C) (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t < 1) : (1 - t) • x + t • y ∈ euclideanRelativeInterior n C

Theorem 6.1: Let C be a convex set in R^n. Let x ∈ ri C and y ∈ cl C. Then (1 - λ) x + λ y belongs to ri C (and hence in particular to C) for 0 ≤ λ < 1.

theorem convex_closure_of_convex (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) : Convex ℝ (closure C)

The closure of a convex set is convex.