def polyhedral_projection_feasible_set {n p : ℕ} (A : Matrix (Fin p) (Fin n) ℝ) (b : EuclideanSpace ℝ (Fin p)) : Set (EuclideanSpace ℝ (Fin n))

Definition 12.8. The polyhedral feasible set S = {x ∈ ℝ^n | A x ≤ b} associated to the matrix inequality system A x ≤ b.

@[simp]

theorem mem_polyhedral_projection_feasible_set {n p : ℕ} (A : Matrix (Fin p) (Fin n) ℝ) (b : EuclideanSpace ℝ (Fin p)) {x : EuclideanSpace ℝ (Fin n)} : x ∈ polyhedral_projection_feasible_set A b ↔ ∀ (i : Fin p), ((Matrix.toEuclideanLin A) x).ofLp i ≤ b.ofLp i

Helper for Definition 12.8: membership in the polyhedral feasible set means satisfying each row inequality A x ≤ b.

theorem polyhedral_projection_feasible_set_eq_setOf {n p : ℕ} (A : Matrix (Fin p) (Fin n) ℝ) (b : EuclideanSpace ℝ (Fin p)) : polyhedral_projection_feasible_set A b = {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin p), ((Matrix.toEuclideanLin A) x).ofLp i ≤ b.ofLp i}

Helper for Definition 12.8: the polyhedral feasible set is exactly the set of points satisfying every row inequality A x ≤ b.