theorem C2_nonempty_of_not_subset_relativeBoundary (n : ℕ) (C1 C2 : Set (EuclideanSpace ℝ (Fin n))) (hC2not : ¬C2 ⊆ euclideanRelativeBoundary n C1) : C2.Nonempty

A set not contained in the relative boundary is nonempty.

theorem euclideanRelativeInterior_ball_subset (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n)} (hx : x ∈ euclideanRelativeInterior n C) : ∃ (ε : ℝ), 0 < ε ∧ (fun (y : EuclideanSpace ℝ (Fin n)) => x + y) '' (ε • euclideanUnitBall n) ∩ ↑(affineSpan ℝ C) ⊆ euclideanRelativeInterior n C

A relative interior point has a smaller ball in the affine span contained in the relative interior.

theorem riC2_inter_riC1_nonempty (n : ℕ) (C1 C2 : Set (EuclideanSpace ℝ (Fin n))) (hC2 : Convex ℝ C2) (hC2sub : C2 ⊆ closure C1) (hC2not : ¬C2 ⊆ euclideanRelativeBoundary n C1) : (euclideanRelativeInterior n C2 ∩ euclideanRelativeInterior n C1).Nonempty

Under the corollary hypotheses, the relative interiors of C1 and C2 intersect.

theorem ri_intersection_fin_two (n : ℕ) (C1 C2 : Set (EuclideanSpace ℝ (Fin n))) (hC1 : Convex ℝ C1) (hC2 : Convex ℝ C2) (hri : (euclideanRelativeInterior n C2 ∩ euclideanRelativeInterior n (closure C1)).Nonempty) : euclideanRelativeInterior n (C2 ∩ closure C1) = euclideanRelativeInterior n C2 ∩ euclideanRelativeInterior n (closure C1)

Relative interiors of two convex sets coincide with the relative interior of their intersection when their relative interiors meet.

theorem euclideanRelativeInterior_subset_of_subset_closure_not_subset_relativeBoundary (n : ℕ) (C1 C2 : Set (EuclideanSpace ℝ (Fin n))) (hC1 : Convex ℝ C1) (hC2 : Convex ℝ C2) (hC2sub : C2 ⊆ closure C1) (hC2not : ¬C2 ⊆ euclideanRelativeBoundary n C1) : euclideanRelativeInterior n C2 ⊆ euclideanRelativeInterior n C1

Corollary 6.5.2. Let C1 be a convex set. Let C2 be a convex set contained in cl C1 but not entirely contained in the relative boundary of C1. Then ri C2 ⊆ ri C1.

theorem image_closure_subset_closure_image_linearMap (n m : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) : ⇑A '' closure C ⊆ closure (⇑A '' C)

Linear maps send closures into the closure of the image.

theorem image_relativeInterior_subset_relativeInterior_image (n m : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) : ⇑A '' euclideanRelativeInterior n C ⊆ euclideanRelativeInterior m (⇑A '' C)

Linear images of relative interior points stay in the relative interior of the image.

theorem closure_image_eq_closure_image_ri (n m : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) : closure (⇑A '' C) = closure (⇑A '' euclideanRelativeInterior n C)

Linear images of a convex set and its relative interior have the same closure.

theorem relativeInterior_image_subset_image_relativeInterior (n m : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) : euclideanRelativeInterior m (⇑A '' C) ⊆ ⇑A '' euclideanRelativeInterior n C

The relative interior of a linear image lies in the image of the relative interior.

theorem euclideanRelativeInterior_image_linearMap_eq_and_image_closure_subset (n m : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) : euclideanRelativeInterior m (⇑A '' C) = ⇑A '' euclideanRelativeInterior n C ∧ ⇑A '' closure C ⊆ closure (⇑A '' C)

Theorem 6.6: Let C be a convex set in R^n, and let A be a linear transformation from R^n to R^m. Then ri (A C) = A (ri C) and cl (A C) ⊇ A (cl C).

theorem ri_image_lsmul_eq (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (r : ℝ) : euclideanRelativeInterior n (⇑((LinearMap.lsmul ℝ (EuclideanSpace ℝ (Fin n))) r) '' C) = ⇑((LinearMap.lsmul ℝ (EuclideanSpace ℝ (Fin n))) r) '' euclideanRelativeInterior n C

Relative interior commutes with LinearMap.lsmul as a linear image.

theorem image_lsmul_eq_smul_set (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (r : ℝ) : ⇑((LinearMap.lsmul ℝ (EuclideanSpace ℝ (Fin n))) r) '' C = r • C

The image of a set under LinearMap.lsmul is pointwise scalar multiplication.

theorem euclideanRelativeInterior_smul (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (r : ℝ) : euclideanRelativeInterior n (r • C) = r • euclideanRelativeInterior n C

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