Rockafellar, §6: Relative Interiors of Convex Sets

Relative interiors and closures of convex sets: the line segment principle, the fact that a non-empty convex set has a non-empty relative interior, and how ri and cl behave under intersection, linear images and inverse images, products, and convex hulls of unions. All 18 numbered results of §6 are formalized.

The book's cl C is Mathlib's closure C, its int C is interior C, and its ri C is the backbone's ri, that is intrinsicInterior ℝ.

Main definitions

• relbd C — the relative boundary (cl C) \ (ri C), bridged to Mathlib's intrinsicFrontier ℝ by relbd_eq_intrinsicFrontier.
• IsRelativelyOpen C — the book's relatively open: ri C = C.
• coneOver C — the convex cone of Corollary 6.8.1, generated by {(1, x) | x ∈ C}.

Theorem 6.2 is where finite-dimensionality enters, and it never leaves. That a non-empty convex set has a non-empty relative interior is false in infinite dimensions — the positive cone of ℓ² is the standard witness — and §§7, 9, 10, 11, 16, 18 and 20 use it without saying so. Every statement below inherits FiniteDimensional ℝ (Rn n) from the ambient instance, so none of them carries a dimension hypothesis of its own, which is what makes the dependence easy to miss.

theorem_6_9 is the two-set case, where the book states the result for m sets. ℝᵐ⁺ᵖ is Rn m × Rn p here, as in §3, so Theorem 6.8 is stated on the product and Corollary 6.8.1 on ℝ × ℝⁿ. Theorems 6.6 and 6.7 take a LinearMap, where the book remarks that affine transformations work too. theorem_6_5_ri adds Finite ι to the book's arbitrary index set: the intersection of ri [0, 1 + α] over all α > 0 is the book's own counterexample to dropping it.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §6.

The relative interior, the relative boundary and relatively open sets

def Rockafellar.relbd {n : ℕ} (C : Set (TdafSurface.Rn n)) : Set (TdafSurface.Rn n)

Rockafellar, §6 (p. 44). The relative boundary of C is (cl C) ∖ (ri C).

Equations

• Rockafellar.relbd C = closure C \ intrinsicInterior ℝ C

theorem Rockafellar.relbd_eq_intrinsicFrontier {n : ℕ} (C : Set (TdafSurface.Rn n)) : relbd C = intrinsicFrontier ℝ C

The bridge: the book's relative boundary is Mathlib's intrinsicFrontier.

theorem Rockafellar.mem_relbd_iff {n : ℕ} {C : Set (TdafSurface.Rn n)} {x : TdafSurface.Rn n} : x ∈ relbd C ↔ x ∈ closure C ∧ x ∉ intrinsicInterior ℝ C

Membership in the relative boundary, spelled out.

def Rockafellar.IsRelativelyOpen {n : ℕ} (C : Set (TdafSurface.Rn n)) : Prop

Rockafellar, §6 (p. 44). C is relatively open when ri C = C.

Equations

• Rockafellar.IsRelativelyOpen C = (intrinsicInterior ℝ C = C)

theorem Rockafellar.isRelativelyOpen_iff {n : ℕ} {C : Set (TdafSurface.Rn n)} : IsRelativelyOpen C ↔ intrinsicInterior ℝ C = C

The bridge: relative openness is the equation ri C = C, by definition.

theorem Rockafellar.relint_subset_subset_closure {n : ℕ} (C : Set (TdafSurface.Rn n)) : intrinsicInterior ℝ C ⊆ C ∧ C ⊆ closure C

Rockafellar, §6 (p. 44). The sandwich ri C ⊆ C ⊆ cl C.

theorem Rockafellar.relint_eq_interior {n : ℕ} {C : Set (TdafSurface.Rn n)} (h : affineSpan ℝ C = ⊤) : intrinsicInterior ℝ C = interior C

Rockafellar, §6 (p. 45). For an n-dimensional convex set aff C = ℝⁿ, and then ri C = int C.

theorem Rockafellar.isRelativelyOpen_of_isAffineSet {n : ℕ} {M : Set (TdafSurface.Rn n)} (h : IsAffineSet M) : IsRelativelyOpen M

Rockafellar, §6 (p. 45). An affine set is relatively open.

theorem Rockafellar.isClosed_of_isAffineSet {n : ℕ} {M : Set (TdafSurface.Rn n)} (h : IsAffineSet M) : IsClosed M

Rockafellar, §6 (p. 45). Every affine set is closed. In the book this is read off from Corollary 1.4.1 and Theorem 1.3; here it is the finite-dimensionality of ℝⁿ.

theorem Rockafellar.closure_subset_affineSpan {n : ℕ} (C : Set (TdafSurface.Rn n)) : closure C ⊆ ↑(affineSpan ℝ C)

Rockafellar, §6 (p. 45). cl C ⊆ cl (aff C) = aff C, so a line through two points of cl C lies in aff C.

Theorem 6.1: the line segment principle

theorem Rockafellar.theorem_6_1 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) {x y : TdafSurface.Rn n} (hx : x ∈ intrinsicInterior ℝ C) (hy : y ∈ closure C) {l : ℝ} (hl₀ : 0 ≤ l) (hl₁ : l < 1) : (1 - l) • x + l • y ∈ intrinsicInterior ℝ C

Theorem 6.1. Let C be a convex set in ℝⁿ, 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 6.2

theorem Rockafellar.theorem_6_2_convex_cl {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) : Convex ℝ (closure C)

Theorem 6.2. cl C is convex.

theorem Rockafellar.theorem_6_2_convex_ri {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) : Convex ℝ (intrinsicInterior ℝ C)

Theorem 6.2. ri C is convex. This is Theorem 6.1 with y taken in ri C.

theorem Rockafellar.theorem_6_2_aff_cl {n : ℕ} (C : Set (TdafSurface.Rn n)) : affineSpan ℝ (closure C) = affineSpan ℝ C

Theorem 6.2. cl C has the same affine hull as C. No convexity is needed.

theorem Rockafellar.theorem_6_2_aff_ri {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) : affineSpan ℝ (intrinsicInterior ℝ C) = affineSpan ℝ C

Theorem 6.2. ri C has the same affine hull as C.

theorem Rockafellar.theorem_6_2_dim_cl {n : ℕ} (C : Set (TdafSurface.Rn n)) : dim (closure C) = dim C

Theorem 6.2. cl C has the same dimension as C.

theorem Rockafellar.theorem_6_2_dim_ri {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) : dim (intrinsicInterior ℝ C) = dim C

Theorem 6.2. ri C has the same dimension as C.

theorem Rockafellar.theorem_6_2_nonempty {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hne : C.Nonempty) : (intrinsicInterior ℝ C).Nonempty

Theorem 6.2, the parenthetical clause: ri C ≠ ∅ when C ≠ ∅. This is the single fact that makes Part II finite-dimensional; it is false in infinite dimensions, and nothing weaker than finite-dimensionality will do.

Theorem 6.3 and its corollaries

theorem Rockafellar.theorem_6_3_cl_ri {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) : closure (intrinsicInterior ℝ C) = closure C

Theorem 6.3. For any convex set C in ℝⁿ, cl (ri C) = cl C.

theorem Rockafellar.theorem_6_3_ri_cl {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) : intrinsicInterior ℝ (closure C) = intrinsicInterior ℝ C

Theorem 6.3. For any convex set C in ℝⁿ, ri (cl C) = ri C.

theorem Rockafellar.isRelativelyOpen_relint {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) : IsRelativelyOpen (intrinsicInterior ℝ C)

Rockafellar, §6 (p. 46). ri (ri C) = ri C: the relative interior of a convex set is relatively open. The book asserts this for arbitrary sets, before Theorem 6.3; the backbone proves it for convex sets, through Theorem 6.3.

theorem Rockafellar.corollary_6_3_1 {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : Convex ℝ C₁) (h₂ : Convex ℝ C₂) : closure C₁ = closure C₂ ↔ intrinsicInterior ℝ C₁ = intrinsicInterior ℝ C₂

Corollary 6.3.1. Let C₁ and C₂ be convex sets in ℝⁿ. Then cl C₁ = cl C₂ if and only if ri C₁ = ri C₂.

theorem Rockafellar.corollary_6_3_1_sandwich {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : Convex ℝ C₁) (h₂ : Convex ℝ C₂) : closure C₁ = closure C₂ ↔ intrinsicInterior ℝ C₁ ⊆ C₂ ∧ C₂ ⊆ closure C₁

Corollary 6.3.1, third condition: the two above are equivalent to ri C₁ ⊆ C₂ ⊆ cl C₁.

theorem Rockafellar.corollary_6_3_2 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) {U : Set (TdafSurface.Rn n)} (hU : IsOpen U) (h : (U ∩ closure C).Nonempty) : (U ∩ intrinsicInterior ℝ C).Nonempty

Corollary 6.3.2. If C is a convex set in ℝⁿ, then every open set which meets cl C also meets ri C.

theorem Rockafellar.inter_relint_nonempty_of_affineSpan_eq {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : Convex ℝ C₁) (hne₁ : C₁.Nonempty) (h₂ : Convex ℝ C₂) (hsub : C₁ ⊆ closure C₂) (hspan : affineSpan ℝ C₁ = affineSpan ℝ C₂) : (C₁ ∩ intrinsicInterior ℝ C₂).Nonempty

A non-empty convex set inside cl C₂ whose affine hull is that of C₂ already meets ri C₂: a relative interior point of C₁ has a ball of aff C₁ = aff C₂ around it inside C₁, and cl C₂ = cl (ri C₂) puts a point of ri C₂ in that ball. The step Corollary 6.3.3 needs.

theorem Rockafellar.corollary_6_3_3 {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : Convex ℝ C₁) (h₂ : Convex ℝ C₂) (hne₂ : C₂.Nonempty) (hsub : C₁ ⊆ relbd C₂) : dim C₁ < dim C₂

Corollary 6.3.3. A convex subset C₁ of the relative boundary of a non-empty convex set C₂ has dim C₁ < dim C₂.

Theorem 6.4: the prolongation criterion

theorem Rockafellar.theorem_6_4 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hne : C.Nonempty) {z : TdafSurface.Rn n} : z ∈ intrinsicInterior ℝ C ↔ ∀ x ∈ C, ∃ μ > 1, (1 - μ) • x + μ • z ∈ C

Theorem 6.4. Let C be a non-empty convex set in ℝⁿ. Then z ∈ ri C if and only if, for every x ∈ C, there exists a μ > 1 such that (1 - μ) x + μ z belongs to C.

theorem Rockafellar.corollary_6_4_1 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) {z : TdafSurface.Rn n} : z ∈ interior C ↔ ∀ (y : TdafSurface.Rn n), ∃ (ε : ℝ), 0 < ε ∧ z + ε • y ∈ C

Corollary 6.4.1. Let C be a convex set in ℝⁿ. Then z ∈ int C if and only if, for every y ∈ ℝⁿ, there exists some ε > 0 such that z + ε y ∈ C.

Theorem 6.5: intersections

theorem Rockafellar.theorem_6_5_cl {n : ℕ} {ι : Type u_1} {C : ι → Set (TdafSurface.Rn n)} (hC : ∀ (i : ι), Convex ℝ (C i)) (h : (⋂ (i : ι), intrinsicInterior ℝ (C i)).Nonempty) : closure (⋂ (i : ι), C i) = ⋂ (i : ι), closure (C i)

Theorem 6.5, the closure formula. Let Cᵢ be a convex set in ℝⁿ for i ∈ I. Suppose that the sets ri Cᵢ have at least one point in common. Then cl ⋂ᵢ Cᵢ = ⋂ᵢ cl Cᵢ. The index set is arbitrary.

theorem Rockafellar.theorem_6_5_ri {n : ℕ} {ι : Type u_1} [Finite ι] {C : ι → Set (TdafSurface.Rn n)} (hC : ∀ (i : ι), Convex ℝ (C i)) (h : (⋂ (i : ι), intrinsicInterior ℝ (C i)).Nonempty) : intrinsicInterior ℝ (⋂ (i : ι), C i) = ⋂ (i : ι), intrinsicInterior ℝ (C i)

Theorem 6.5, the relative interior formula: if in addition I is finite, ri ⋂ᵢ Cᵢ = ⋂ᵢ ri Cᵢ. Finiteness cannot be dropped — the book's own counterexample is the family [0, 1 + α] for α > 0.

theorem Rockafellar.corollary_6_5_1_ri {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) {M : Set (TdafSurface.Rn n)} (hM : IsAffineSet M) (h : (M ∩ intrinsicInterior ℝ C).Nonempty) : intrinsicInterior ℝ (M ∩ C) = M ∩ intrinsicInterior ℝ C

Corollary 6.5.1. Let C be a convex set, and let M be an affine set (such as a line or a hyperplane) which contains a point of ri C. Then ri (M ∩ C) = M ∩ ri C.

theorem Rockafellar.corollary_6_5_1_cl {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) {M : Set (TdafSurface.Rn n)} (hM : IsAffineSet M) (h : (M ∩ intrinsicInterior ℝ C).Nonempty) : closure (M ∩ C) = M ∩ closure C

Corollary 6.5.1, the closure half: cl (M ∩ C) = M ∩ cl C.

theorem Rockafellar.corollary_6_5_2 {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : Convex ℝ C₁) (h₂ : Convex ℝ C₂) (hsub : C₂ ⊆ closure C₁) (hnb : ¬C₂ ⊆ relbd C₁) : intrinsicInterior ℝ C₂ ⊆ intrinsicInterior ℝ C₁

Corollary 6.5.2. For convex C₂ ⊆ cl C₁ not entirely contained in the relative boundary of C₁, ri C₂ ⊆ ri C₁. The hypothesis is the positive reading (C₂ ∩ ri C₁).Nonempty of "not entirely contained in the relative boundary".

Theorem 6.6: images under a linear transformation

theorem Rockafellar.theorem_6_6_ri {n m : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m) : intrinsicInterior ℝ (⇑A '' C) = ⇑A '' intrinsicInterior ℝ C

Theorem 6.6. Let C be a convex set in ℝⁿ, and let A be a linear transformation from ℝⁿ to ℝᵐ. Then ri (AC) = A (ri C).

theorem Rockafellar.theorem_6_6_cl {n m : ℕ} (C : Set (TdafSurface.Rn n)) (A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m) : ⇑A '' closure C ⊆ closure (⇑A '' C)

Theorem 6.6. cl (AC) ⊇ A (cl C). This is just continuity of A and needs no convexity.

theorem Rockafellar.corollary_6_6_1 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (l : ℝ) : intrinsicInterior ℝ (l • C) = l • intrinsicInterior ℝ C

Corollary 6.6.1. For any convex set C and any real number λ, ri (λ C) = λ (ri C).

theorem Rockafellar.relint_prod {n m : ℕ} (D₁ : Set (TdafSurface.Rn n)) (D₂ : Set (TdafSurface.Rn m)) : intrinsicInterior ℝ (D₁ ×ˢ D₂) = intrinsicInterior ℝ D₁ ×ˢ intrinsicInterior ℝ D₂

Rockafellar, §6 (p. 49). The direct-sum formula the book calls "elementary": ri (C₁ ⊕ C₂) = ri C₁ ⊕ ri C₂.

theorem Rockafellar.closure_prod {n m : ℕ} (D₁ : Set (TdafSurface.Rn n)) (D₂ : Set (TdafSurface.Rn m)) : closure (D₁ ×ˢ D₂) = closure D₁ ×ˢ closure D₂

Rockafellar, §6 (p. 49). cl (C₁ ⊕ C₂) = cl C₁ ⊕ cl C₂.

theorem Rockafellar.corollary_6_6_2_ri {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : Convex ℝ C₁) (h₂ : Convex ℝ C₂) : intrinsicInterior ℝ (C₁ + C₂) = intrinsicInterior ℝ C₁ + intrinsicInterior ℝ C₂

Corollary 6.6.2. For any convex sets C₁ and C₂ in ℝⁿ, ri (C₁ + C₂) = ri C₁ + ri C₂.

theorem Rockafellar.corollary_6_6_2_cl {n : ℕ} (D₁ D₂ : Set (TdafSurface.Rn n)) : closure D₁ + closure D₂ ⊆ closure (D₁ + D₂)

Corollary 6.6.2. cl (C₁ + C₂) ⊇ cl C₁ + cl C₂. No convexity is needed. Corollary 9.1.1 sharpens this to an equality.

Theorem 6.7: inverse images under a linear transformation

theorem Rockafellar.theorem_6_7_ri {n m : ℕ} {D : Set (TdafSurface.Rn m)} (hD : Convex ℝ D) (A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m) (h : (⇑A ⁻¹' intrinsicInterior ℝ D).Nonempty) : intrinsicInterior ℝ (⇑A ⁻¹' D) = ⇑A ⁻¹' intrinsicInterior ℝ D

Theorem 6.7. Let A be a linear transformation from ℝⁿ to ℝᵐ. Let C be a convex set in ℝᵐ such that A⁻¹(ri C) ≠ ∅. Then ri (A⁻¹C) = A⁻¹(ri C).

theorem Rockafellar.theorem_6_7_cl {n m : ℕ} {D : Set (TdafSurface.Rn m)} (hD : Convex ℝ D) (A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m) (h : (⇑A ⁻¹' intrinsicInterior ℝ D).Nonempty) : closure (⇑A ⁻¹' D) = ⇑A ⁻¹' closure D

Theorem 6.7. Under the same hypothesis, cl (A⁻¹C) = A⁻¹(cl C).

Theorem 6.8: slices of a convex set in a product

theorem Rockafellar.theorem_6_8 {m p : ℕ} {C : Set (TdafSurface.Rn m × TdafSurface.Rn p)} (hC : Convex ℝ C) (y : TdafSurface.Rn m) (z : TdafSurface.Rn p) : (y, z) ∈ intrinsicInterior ℝ C ↔ y ∈ intrinsicInterior ℝ {u : TdafSurface.Rn m | {w : TdafSurface.Rn p | (u, w) ∈ C}.Nonempty} ∧ z ∈ intrinsicInterior ℝ {w : TdafSurface.Rn p | (y, w) ∈ C}

Theorem 6.8. For convex C ⊆ ℝᵐ⁺ᵖ with slices C_y = {z | (y, z) ∈ C} and D = {y | C_y ≠ ∅}, (y, z) ∈ ri C iff y ∈ ri D and z ∈ ri C_y.

def Rockafellar.coneOver {n : ℕ} (C : Set (TdafSurface.Rn n)) : Set (ℝ × TdafSurface.Rn n)

Corollary 6.8.1. The convex cone K in ℝⁿ⁺¹ generated by {(1, x) | x ∈ C}. Rockafellar's cones need not contain the origin, so K is the set of positive multiples of the cross-section, and nothing more.

Equations

• Rockafellar.coneOver C = {q : ℝ × TdafSurface.Rn n | 0 < q.1 ∧ q.2 ∈ q.1 • C}

theorem Rockafellar.mem_coneOver_iff {n : ℕ} {C : Set (TdafSurface.Rn n)} {q : ℝ × TdafSurface.Rn n} : q ∈ coneOver C ↔ ∃ (l : ℝ), 0 < l ∧ ∃ x ∈ C, l • (1, x) = q

The bridge: coneOver C is exactly the set of positive multiples of {(1, x) | x ∈ C}, which is what Corollary 2.6.3 identifies as the smallest convex cone containing that set.

theorem Rockafellar.convex_coneOver {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) : Convex ℝ (coneOver C)

coneOver C is convex when C is: it is the intersection of the backbone's cone (which carries the origin) with the open half-space {q | 0 < q.1}.

theorem Rockafellar.corollary_6_8_1 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hne : C.Nonempty) : intrinsicInterior ℝ (coneOver C) = {q : ℝ × TdafSurface.Rn n | 0 < q.1 ∧ q.2 ∈ q.1 • intrinsicInterior ℝ C}

Corollary 6.8.1. For non-empty convex C and K the convex cone in ℝⁿ⁺¹ generated by {(1, x) | x ∈ C}, ri K is the set of (λ, x) with λ > 0 and x ∈ λ (ri C).

Theorem 6.9

theorem Rockafellar.theorem_6_9 {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : Convex ℝ C₁) (hne₁ : C₁.Nonempty) (h₂ : Convex ℝ C₂) (hne₂ : C₂.Nonempty) : intrinsicInterior ℝ ((convexHull ℝ) (C₁ ∪ C₂)) = ⋃ (l₁ : ℝ), ⋃ (l₂ : ℝ), ⋃ (_ : 0 < l₁), ⋃ (_ : 0 < l₂), ⋃ (_ : l₁ + l₂ = 1), l₁ • intrinsicInterior ℝ C₁ + l₂ • intrinsicInterior ℝ C₂

Theorem 6.9, for two sets. For non-empty convex C₁, C₂ and C₀ = conv (C₁ ∪ C₂), ri C₀ = ⋃ {λ₁ ri C₁ + λ₂ ri C₂ | λᵢ > 0, λ₁ + λ₂ = 1}, the union written in the parametrised form λ₁ = 1 - a, λ₂ = a with a ∈ (0, 1). The book states the theorem for m sets.

The relatively open sets of §6

The book closes the section (p. 49) by noting that relative openness is preserved by the operations above, and that the relative interior and the closure of a convex cone are again convex cones.

theorem Rockafellar.isRelativelyOpen_iInter {n : ℕ} {ι : Type u_1} [Finite ι] {C : ι → Set (TdafSurface.Rn n)} (hC : ∀ (i : ι), Convex ℝ (C i)) (hopen : ∀ (i : ι), IsRelativelyOpen (C i)) (h : (⋂ (i : ι), C i).Nonempty) : IsRelativelyOpen (⋂ (i : ι), C i)

Rockafellar, §6 (p. 49). The class of relatively open convex sets is preserved under finite intersections, provided the relative interiors meet — which for relatively open sets is just non-emptiness of the intersection.

theorem Rockafellar.isRelativelyOpen_add {n : ℕ} {C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : Convex ℝ C₁) (h₂ : Convex ℝ C₂) (ho₁ : IsRelativelyOpen C₁) (ho₂ : IsRelativelyOpen C₂) : IsRelativelyOpen (C₁ + C₂)

Rockafellar, §6 (p. 49). The class of relatively open convex sets is preserved under addition.

theorem Rockafellar.isCone_relint {n : ℕ} {C : Set (TdafSurface.Rn n)} (hK : IsCone C) (hC : Convex ℝ C) : IsCone (intrinsicInterior ℝ C)

Rockafellar, §6 (p. 50). The relative interior of a convex cone is a convex cone. This is immediate from Corollary 6.6.1, because a convex set C is a cone exactly when λ C = C for every λ > 0 (§2's isCone_iff_smul_set_eq).

theorem Rockafellar.isCone_closure {n : ℕ} {C : Set (TdafSurface.Rn n)} (hK : IsCone C) : IsCone (closure C)

Rockafellar, §6 (p. 50). The closure of a convex cone is a convex cone. Convexity is not used on either side.