theorem HamSandwich.ham_sandwich_finite (n : ℕ) (hn : 0 < n) (N : ℕ) (S : Fin N → Finset (Fin n → ℝ)) : ∃ (p : MvPolynomial (Fin n) ℝ), p ≠ 0 ∧ ∀ (i : Fin N), {x ∈ S i | (MvPolynomial.eval x) p > 0}.card ≤ (S i).card / 2 ∧ {x ∈ S i | (MvPolynomial.eval x) p < 0}.card ≤ (S i).card / 2

Lemma (Ham Sandwich theorem for finite sets). Given finite sets S₁, …, S_N ⊆ ℝⁿ (n ≥ 1), there exists a nonzero polynomial p ∈ ℝ[x₁,…,xₙ] such that its zero set bisects each Sᵢ: namely $|S_i \cap \{p > 0\}| \le |S_i|/2$ and $|S_i \cap \{p < 0\}| \le |S_i|/2$.

The proof picks the product polynomial vanishing on every point of ⋃ᵢ Sᵢ along the first coordinate, so each side has cardinality 0.