OAI/Combinatorics/IndependentSets/Repetition/FiniteGame.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.finiteGame line 8
  2. lemma OAI.LargeIndependentSets.finiteGame_integral_left line 12
  3. lemma OAI.LargeIndependentSets.finiteGame_integral_right line 19
  4. def OAI.LargeIndependentSets.finiteProbabilitySimplex line 27
  5. lemma OAI.LargeIndependentSets.convex_finiteProbabilitySimplex line 30
  6. lemma OAI.LargeIndependentSets.isCompact_finiteProbabilitySimplex line 38
  7. lemma OAI.LargeIndependentSets.single_mem_finiteProbabilitySimplex line 45
  8. theorem OAI.LargeIndependentSets.finite_minimax_counterstatement line 53