Finite convex separation

The separation lemma used in Scott's proof of Theorem 1.1.

theorem Scott1964.MeasurementStructures.LinearInequalities.finite_strict_separation {L : Type u_1} [NormedAddCommGroup L] [NormedSpace ℝ L] [FiniteDimensional ℝ L] {A B : Set L} (hA : A.Finite) : Disjoint ((convexHull ℝ) A) ↑(Submodule.span ℝ B) ↔ ∃ (φ : Module.Dual ℝ L), (∀ x ∈ A, 0 < φ x) ∧ ∀ x ∈ B, φ x = 0

A finite set A can be made strictly positive while B is made zero exactly when its convex hull misses the span of B.