theorem isClosed_nonneg_cone_image {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) : IsClosed {b : Fin m → ℝ | ∃ (x : Fin n → ℝ), (∀ (j : Fin n), 0 ≤ x j) ∧ A.mulVec x = b}

theorem clm_repr {m : ℕ} (f : (Fin m → ℝ) →L[ℝ] ℝ) (v : Fin m → ℝ) : f v = (fun (i : Fin m) => f (Pi.single i 1)) ⬝ᵥ v

theorem farkas_lemma {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) : (∃ (x : Fin n → ℝ), (∀ (j : Fin n), 0 ≤ x j) ∧ A.mulVec x = b) ↔ ¬∃ (y : Fin m → ℝ), (∀ (j : Fin n), 0 ≤ A.transpose.mulVec y j) ∧ b ⬝ᵥ y < 0