theorem cor11_5_2_disjoint_intrinsicInterior_singleton {n : ℕ} {a : Fin n → ℝ} {C : Set (Fin n → ℝ)} (ha : a ∉ C) : Disjoint (intrinsicInterior ℝ {a}) (intrinsicInterior ℝ C)

If a ∉ C, then {a} and C have disjoint intrinsic interiors.

theorem cor11_5_2_exists_hyperplaneSeparatesProperly_point {n : ℕ} {C : Set (Fin n → ℝ)} {a : Fin n → ℝ} (hCne : C.Nonempty) (hCconv : Convex ℝ C) (ha : a ∉ C) : ∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesProperly n H {a} C

A point outside a nonempty convex set can be properly separated from it by a hyperplane.

theorem cor11_5_2_extract_closedHalfspace_from_separation {n : ℕ} {C : Set (Fin n → ℝ)} {a : Fin n → ℝ} {H : Set (Fin n → ℝ)} (hsep : HyperplaneSeparatesProperly n H {a} C) : ∃ (b : Fin n → ℝ) (β : ℝ), b ≠ 0 ∧ C ⊆ {x : Fin n → ℝ | x ⬝ᵥ b ≤ β}

From a proper separating hyperplane between {a} and C, extract a nontrivial closed half-space of the form {x | x ⬝ᵥ b ≤ β} containing C.

theorem exists_closedHalfspace_superset_of_convex_ne_univ (n : ℕ) (C : Set (Fin n → ℝ)) (hn : 0 < n) (hCconv : Convex ℝ C) (hCne : C ≠ Set.univ) : ∃ (b : Fin n → ℝ) (β : ℝ), b ≠ 0 ∧ C ⊆ {x : Fin n → ℝ | x ⬝ᵥ b ≤ β}

Corollary 11.5.2. Let C be a convex subset of ℝ^n other than ℝ^n itself. Then there exists a closed half-space containing C. In other words, there exists some b ∈ ℝ^n such that the linear function x ↦ ⟪x, b⟫ (i.e. x ⬝ᵥ b) is bounded above on C.

theorem exists_nontrivialSupportingHyperplane_containing_iff_exists_hyperplaneSeparatesProperly {n : ℕ} {C D : Set (Fin n → ℝ)} (hDne : D.Nonempty) (hDC : D ⊆ C) : (∃ (H : Set (Fin n → ℝ)), IsNontrivialSupportingHyperplane n C H ∧ D ⊆ H) ↔ ∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesProperly n H D C

If D ⊆ C, a nontrivial supporting hyperplane to C containing D is the same as a properly separating hyperplane between D and C.

theorem disjoint_intrinsicInterior_left_iff_disjoint_of_subset {n : ℕ} {C D : Set (Fin n → ℝ)} (hCconv : Convex ℝ C) (hDne : D.Nonempty) (hDconv : Convex ℝ D) (hDC : D ⊆ C) : Disjoint (intrinsicInterior ℝ D) (intrinsicInterior ℝ C) ↔ Disjoint D (intrinsicInterior ℝ C)

If D ⊆ C, then ri D is disjoint from ri C iff D is disjoint from ri C.

theorem exists_nontrivialSupportingHyperplane_containing_iff_disjoint_intrinsicInterior (n : ℕ) (C D : Set (Fin n → ℝ)) (hCconv : Convex ℝ C) (hDne : D.Nonempty) (hDconv : Convex ℝ D) (hDC : D ⊆ C) : (∃ (H : Set (Fin n → ℝ)), IsNontrivialSupportingHyperplane n C H ∧ D ⊆ H) ↔ Disjoint D (intrinsicInterior ℝ C)

Theorem 11.6: Let C be a convex set, and let D be a non-empty convex subset of C (for instance, a subset consisting of a single point). In order that there exist a non-trivial supporting hyperplane to C containing D, it is necessary and sufficient that D be disjoint from ri C (the relative/intrinsic interior of C).