theorem intrinsicInterior_eq_euclideanRelativeInterior (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) : intrinsicInterior ℝ C = euclideanRelativeInterior n C

intrinsicInterior equals euclideanRelativeInterior in Euclidean space.

theorem intrinsicInterior_sub_eq (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) (hC₁ : Convex ℝ C₁) (hC₂ : Convex ℝ C₂) : intrinsicInterior ℝ (C₁ - C₂) = intrinsicInterior ℝ C₁ - intrinsicInterior ℝ C₂

Relative interior commutes with Minkowski subtraction for convex sets in Fin n → ℝ.

theorem disjoint_intrinsicInterior_iff_zero_not_mem_intrinsicInterior_sub (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) (hC₁ : Convex ℝ C₁) (hC₂ : Convex ℝ C₂) : Disjoint (intrinsicInterior ℝ C₁) (intrinsicInterior ℝ C₂) ↔ 0 ∉ intrinsicInterior ℝ (C₁ - C₂)

Disjointness of intrinsic interiors is equivalent to 0 not lying in the intrinsic interior of the Minkowski difference.

theorem exists_isOpen_inter_affineSpan_eq_intrinsicInterior (n : ℕ) (s : Set (Fin n → ℝ)) : ∃ (U : Set (Fin n → ℝ)), IsOpen U ∧ intrinsicInterior ℝ s = U ∩ ↑(affineSpan ℝ s)

intrinsicInterior is relatively open in its affine span.

theorem convex_intrinsicInterior_of_convex (n : ℕ) (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) : Convex ℝ (intrinsicInterior ℝ C)

The intrinsic interior of a convex set in Fin n → ℝ is convex.

theorem affineSpan_intrinsicInterior_eq_of_convex_nonempty (n : ℕ) (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (hCne : C.Nonempty) : affineSpan ℝ (intrinsicInterior ℝ C) = affineSpan ℝ C

For a nonempty convex set in Fin n → ℝ, the affine span of the intrinsic interior equals the affine span of the set.

theorem closure_subset_closure_intrinsicInterior_of_convex_nonempty (n : ℕ) (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (hCne : C.Nonempty) : closure C ⊆ closure (intrinsicInterior ℝ C)

For a nonempty convex set in Fin n → ℝ, closure C ⊆ closure (intrinsicInterior C).

theorem zero_not_mem_intrinsicInterior_sub_of_exists_hyperplaneSeparatesProperly (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) : (∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesProperly n H C₁ C₂) → 0 ∉ intrinsicInterior ℝ (C₁ - C₂)

Proper separation implies 0 is not in the intrinsic interior of the Minkowski difference.

theorem exists_hyperplaneSeparatesProperly_of_zero_not_mem_intrinsicInterior_sub (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) (hC₁conv : Convex ℝ C₁) (hC₂conv : Convex ℝ C₂) : 0 ∉ intrinsicInterior ℝ (C₁ - C₂) → ∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesProperly n H C₁ C₂

If 0 is not in the intrinsic interior of the Minkowski difference, then the sets admit a properly separating hyperplane.

theorem exists_hyperplaneSeparatesProperly_iff_disjoint_intrinsicInterior (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) (hC₁conv : Convex ℝ C₁) (hC₂conv : Convex ℝ C₂) : (∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesProperly n H C₁ C₂) ↔ Disjoint (intrinsicInterior ℝ C₁) (intrinsicInterior ℝ C₂)

Theorem 11.3: Let C₁ and C₂ be non-empty convex sets in ℝ^n. In order that there exist a hyperplane separating C₁ and C₂ properly, it is necessary and sufficient that ri C₁ and ri C₂ have no point in common, where ri denotes the relative (intrinsic) interior.