def separates {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S₁ S₂ : Set E) (p : E) (α : ℝ) : Prop

separates S₁ S₂ p α means the genuine sunYuanHyperplane sunYuanHyperplane p α, with nonzero normal p, leaves S₁ in the closed upper half-space and S₂ in the closed lower half-space determined by p and α.

def properlySeparates {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S₁ S₂ : Set E) (p : E) (α : ℝ) : Prop

properlySeparates S₁ S₂ p α means sunYuanHyperplane p α separates S₁ and S₂, and some point of S₁ ∪ S₂ lies off the sunYuanHyperplane. As in Definition 1.3.23, the canonical core is that the relevant set is not contained in the sunYuanHyperplane.

def strictlySeparates {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S₁ S₂ : Set E) (p : E) (α : ℝ) : Prop

strictlySeparates S₁ S₂ p α means the genuine sunYuanHyperplane sunYuanHyperplane p α, with nonzero normal p, puts the points of S₁ and S₂ in opposite open half-spaces.

def stronglySeparates {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S₁ S₂ : Set E) (p : E) (α : ℝ) : Prop

stronglySeparates S₁ S₂ p α means the genuine sunYuanHyperplane sunYuanHyperplane p α, with nonzero normal p, admits a positive margin ε for which α + ε ≤ ⟪p, x⟫ on S₁ and ⟪p, x⟫ ≤ α on S₂.

theorem separates_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S₁ S₂ : Set E} {p : E} {α : ℝ} : separates S₁ S₂ p α ↔ p ≠ 0 ∧ (∀ x ∈ S₁, α ≤ inner ℝ p x) ∧ ∀ x ∈ S₂, inner ℝ p x ≤ α

Chapter01 Definition 1.3.26 (1): the source states this for nonempty convex subsets of ℝ^n, but the defining separation condition itself only uses the real inner-product-space sunYuanHyperplane data p ≠ 0 together with the two half-space inclusions. The sunYuanHyperplane sunYuanHyperplane p α separates S₁ and S₂ exactly when p ≠ 0, α ≤ ⟪p, x⟫ for all x ∈ S₁, and ⟪p, x⟫ ≤ α for all x ∈ S₂.

theorem properlySeparates_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S₁ S₂ : Set E} {p : E} {α : ℝ} : properlySeparates S₁ S₂ p α ↔ separates S₁ S₂ p α ∧ ∃ x ∈ S₁ ∪ S₂, x ∉ sunYuanHyperplane p α

Chapter01 Definition 1.3.26 (2): the source states this for nonempty convex subsets of ℝ^n, but the proper-separation clause itself only adds that some point of S₁ ∪ S₂ lies off the sunYuanHyperplane.

theorem properlySeparates_iff_not_subset_sunYuanHyperplane {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S₁ S₂ : Set E} {p : E} {α : ℝ} : properlySeparates S₁ S₂ p α ↔ separates S₁ S₂ p α ∧ ¬S₁ ∪ S₂ ⊆ sunYuanHyperplane p α

The source's “some point lies off the sunYuanHyperplane” clause is equivalent to saying that S₁ ∪ S₂ is not contained in sunYuanHyperplane p α.

theorem strictlySeparates_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S₁ S₂ : Set E} {p : E} {α : ℝ} : strictlySeparates S₁ S₂ p α ↔ p ≠ 0 ∧ (∀ x ∈ S₁, α < inner ℝ p x) ∧ ∀ x ∈ S₂, inner ℝ p x < α

Chapter01 Definition 1.3.26 (3): the source states this for nonempty convex subsets of ℝ^n, but the defining strict-separation condition itself only uses the real inner-product-space sunYuanHyperplane data p ≠ 0 together with the open half-space inclusions. The sunYuanHyperplane sunYuanHyperplane p α strictly separates S₁ and S₂ exactly when p ≠ 0, α < ⟪p, x⟫ for all x ∈ S₁, and ⟪p, x⟫ < α for all x ∈ S₂.

theorem stronglySeparates_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S₁ S₂ : Set E} {p : E} {α : ℝ} : stronglySeparates S₁ S₂ p α ↔ p ≠ 0 ∧ ∃ ε > 0, (∀ x ∈ S₁, α + ε ≤ inner ℝ p x) ∧ ∀ x ∈ S₂, inner ℝ p x ≤ α

Chapter01 Definition 1.3.26 (4): the source states this for nonempty convex subsets of ℝ^n, but the defining strong-separation condition itself only uses the real inner-product-space sunYuanHyperplane data p ≠ 0 together with the margin inequality. The sunYuanHyperplane sunYuanHyperplane p α strongly separates S₁ and S₂ exactly when p ≠ 0 and there exists ε > 0 such that α + ε ≤ ⟪p, x⟫ for all x ∈ S₁ and ⟪p, x⟫ ≤ α for all x ∈ S₂.