Lemma 6.6.1 — a minimally infeasible system is tight off each dropped row

Proved

MatousekLP.Duality.minimally_infeasible_tight

by mikedeng1 · Oct 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-inequalitieslinear-programmingp2o-batch-b23bp2o-gran-per-chapterp2o-plan-bookp2o-v1

Let $Ax\le b$ be a minimally infeasible system of $m$ inequalities $a_i^{T}x\le b_i$ (it has no solution, but dropping any single inequality leaves a solvable system). For $i=1,\dots,m$ let $A^{(i)}x\le b^{(i)}$ be the subsystem obtained by dropping the $i$ th inequality. Then for every $i$ there is a vector $\tilde x^{(i)}\in\mathbb{R}^n$ with

A^{(i)}\tilde x^{(i)}=b^{(i)},\qquad\text{i.e.}\qquad a_j^{T}\tilde x^{(i)}=b_j \ \text{ for all } j\ne i.

Together with Lemma 6.6.2 this yields the third proof of the Farkas lemma, variant (iii) of Proposition 6.4.3.

Formalization Note Rows are indexed by Fin m (the book's $1,\dots,m$ are $0,\dots,m-1$ ). Minimal infeasibility is the definition MatousekLP.Duality.IsMinimallyInfeasible; for $m=0$ the empty system is solvable, so the hypothesis cannot hold, exactly as in the book.

Preamble

import Mathlib
import Definitions.Def_MatousekLP_Duality_MinimallyInfeasible

Formal statement

namespace MatousekLP.Duality

open Matrix

/-- Matoušek & Gärtner, Lemma 6.6.1 (p. 98): if `Ax ≤ b` is a minimally infeasible system of `m`
inequalities and `A⁽ⁱ⁾x ≤ b⁽ⁱ⁾` is the subsystem with the `i`th inequality dropped, then for every
`i` there is a vector `x̃⁽ⁱ⁾` with `A⁽ⁱ⁾x̃⁽ⁱ⁾ = b⁽ⁱ⁾`, i.e. `(Ax̃⁽ⁱ⁾)_j = b_j` for every `j ≠ i`. -/
theorem minimally_infeasible_tight {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ)
    (h : IsMinimallyInfeasible A b) :
    ∀ i : Fin m, ∃ x : Fin n → ℝ, ∀ j : Fin m, j ≠ i → (A *ᵥ x) j = b j := by sorry

end MatousekLP.Duality

Source

Matoušek & Gärtner, Understanding and Using Linear Programming, Springer 2007, p. 98, Lemma 6.6.1 (definition of minimally infeasible on p. 97)

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph