theorem isBounded_inter_line_of_rb_endpoints_with_ri_point {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) {x₁ x₂ : EuclideanSpace ℝ (Fin n)} (hx₁rb : x₁ ∈ euclideanRelativeBoundary n C) (hx₂rb : x₂ ∈ euclideanRelativeBoundary n C) (hri : ∃ y ∈ euclideanRelativeInterior n C, y ∈ openSegment ℝ x₁ x₂) : Bornology.IsBounded (↑(AffineSubspace.mk' x₁ (ℝ ∙ (x₂ - x₁))) ∩ C)

The line through two boundary points with a relative interior point on their open segment has bounded intersection with C.

theorem exists_rb_endpoints_for_bounded_parallel_line_slice_through_ri {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (M : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) (hMbdd : Bornology.IsBounded (↑M ∩ C)) (hMne : (↑M ∩ C).Nonempty) (hv : ∃ (v : EuclideanSpace ℝ (Fin n)), v ≠ 0 ∧ v ∈ M.direction ∧ v ∈ (affineSpan ℝ C).direction) ⦃x : EuclideanSpace ℝ (Fin n)⦄ : x ∈ euclideanRelativeInterior n C → ∃ (y : EuclideanSpace ℝ (Fin n)) (z : EuclideanSpace ℝ (Fin n)), y ∈ euclideanRelativeBoundary n C ∧ z ∈ euclideanRelativeBoundary n C ∧ x ∈ segment ℝ y z

A bounded line-slice parallel to M through a relative interior point yields boundary endpoints whose segment contains that point.

theorem exists_mem_segment_of_mem_euclideanRelativeInterior {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hC_not_affine : ¬∃ (A : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))), ↑A = C) (hC_not_closedHalf_affine : ¬∃ (A : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) (f : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] ℝ) (a : ℝ), f ≠ 0 ∧ C = ↑A ∩ {x : EuclideanSpace ℝ (Fin n) | f x ≤ a}) ⦃x : EuclideanSpace ℝ (Fin n)⦄ : x ∈ euclideanRelativeInterior n C → ∃ (y : EuclideanSpace ℝ (Fin n)) (z : EuclideanSpace ℝ (Fin n)), y ∈ euclideanRelativeBoundary n C ∧ z ∈ euclideanRelativeBoundary n C ∧ x ∈ segment ℝ y z

Theorem 18.4. Let C be a closed convex set which is neither an affine set nor a closed half of an affine set. Then every relative interior point of C lies on a line segment segment ℝ y z joining two relative boundary points y, z ∈ rb C (here ri C/rb C are formalized as euclideanRelativeInterior/euclideanRelativeBoundary).