theorem exists_strictSep_point_of_mem_affineSpan_openIn_convex (n : ℕ) (C : Set (Fin n → ℝ)) (D : Submodule ℝ (Fin n → ℝ)) (hCne : C.Nonempty) (hCconv : Convex ℝ C) (hCrelopen : ∃ (U : Set (Fin n → ℝ)), IsOpen U ∧ C = U ∩ ↑(affineSpan ℝ C)) {m0 : Fin n → ℝ} (hq0S : D.mkQ m0 ∉ ⇑D.mkQ '' C) (hq0A : D.mkQ m0 ∈ affineSpan ℝ (⇑D.mkQ '' C)) : ∃ (f : StrongDual ℝ ((Fin n → ℝ) ⧸ D)), ∀ c ∈ C, f (D.mkQ c) < f (D.mkQ m0)

Hard-case separation: in the quotient by a submodule, a convex relatively open set C can be strictly separated from a point in the affine span of its image but outside the image.

theorem exists_strictSep_point_image_mkQ_of_disjoint_convex_relativelyOpen (n : ℕ) (C : Set (Fin n → ℝ)) (M : AffineSubspace ℝ (Fin n → ℝ)) (hCne : C.Nonempty) (hCconv : Convex ℝ C) (hCrelopen : ∃ (U : Set (Fin n → ℝ)), IsOpen U ∧ C = U ∩ ↑(affineSpan ℝ C)) {m0 : Fin n → ℝ} (hm0 : m0 ∈ M) (hCM : Disjoint C ↑M) : ∃ (f : StrongDual ℝ ((Fin n → ℝ) ⧸ M.direction)), (∀ c ∈ C, f (M.direction.mkQ c) < f (M.direction.mkQ m0)) ∨ ∀ c ∈ C, f (M.direction.mkQ m0) < f (M.direction.mkQ c)

Key separation lemma for Theorem 11.2 (to be filled): in the quotient by M.direction, the convex relatively-open set C can be strictly separated from the point corresponding to M.

theorem strongDual_apply_eq_sum_mul_single {n : ℕ} (g : StrongDual ℝ (Fin n → ℝ)) (x : Fin n → ℝ) : g x = ∑ i : Fin n, x i * g (Pi.single i 1)

A continuous linear functional on ℝ^n is determined by its values on the coordinate vectors.

theorem strongDual_apply_eq_dotProduct {n : ℕ} (g : StrongDual ℝ (Fin n → ℝ)) (x : Fin n → ℝ) : g x = x ⬝ᵥ fun (i : Fin n) => g (Pi.single i 1)

Convert a continuous linear functional on ℝ^n into a dotProduct against a vector.

theorem exists_hyperplane_contains_affine_of_convex_relativelyOpen (n : ℕ) (C : Set (Fin n → ℝ)) (M : AffineSubspace ℝ (Fin n → ℝ)) (hCne : C.Nonempty) (hCconv : Convex ℝ C) (hCrelopen : ∃ (U : Set (Fin n → ℝ)), IsOpen U ∧ C = U ∩ ↑(affineSpan ℝ C)) (hMne : (↑M).Nonempty) (hCM : Disjoint C ↑M) : ∃ (H : Set (Fin n → ℝ)), ↑M ⊆ H ∧ ∃ (b : Fin n → ℝ) (β : ℝ), b ≠ 0 ∧ H = {x : Fin n → ℝ | x ⬝ᵥ b = β} ∧ (C ⊆ {x : Fin n → ℝ | x ⬝ᵥ b < β} ∨ C ⊆ {x : Fin n → ℝ | β < x ⬝ᵥ b})

Theorem 11.2: Let C be a non-empty relatively open convex set in R^n, and let M be a non-empty affine set in R^n not meeting C. Then there exists a hyperplane H containing M, such that one of the open half-spaces associated with H contains C.

theorem set_sub_eq_add_neg {E : Type u_1} [AddGroup E] (A B : Set E) : A - B = A + -B

Minkowski subtraction is Minkowski addition with pointwise negation.

theorem neg_set_eq_smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) : -C = -1 • C

Pointwise negation equals scalar multiplication by -1.

theorem ContinuousLinearEquiv.image_intrinsicInterior {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : E ≃L[𝕜] F) (s : Set E) : intrinsicInterior 𝕜 (⇑e '' s) = ⇑e '' intrinsicInterior 𝕜 s

A continuous linear equivalence maps intrinsic interiors.