Covering-row lemma

If the minimax value is strictly positive, every column has a row that Bool-covers it. Used as the starting point for the covering-based minimax bound.

theorem ProbabilityTheory.exists_covering_row {R : Type u_1} {C : Type u_2} [Fintype R] [Fintype C] [DecidableEq C] [Nonempty C] (M : R → C → Bool) (v : ℝ) (hv : 0 < v) (hrow : ∀ (q : FintypePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0) (c₀ : C) : ∃ (r : R), M r c₀ = true

If the minimax value is positive, every column admits a pure row with payoff one.