OAI/Computability/VertexCover/Repetition/SelectionSequence.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniqueGames.Foundations.Repetition.SelectionSequence.exists_unused line 43
  2. def OAI.UniqueGames.Foundations.Repetition.SelectionSequence.nextSet line 59
  3. def OAI.UniqueGames.Foundations.Repetition.SelectionSequence.selectedSet line 65
  4. theorem OAI.UniqueGames.Foundations.Repetition.SelectionSequence.selectedSet_card line 71
  5. theorem OAI.UniqueGames.Foundations.Repetition.SelectionSequence.selectedSet_subset_succ line 94
  6. theorem OAI.UniqueGames.Foundations.Repetition.SelectionSequence.selectedSet_monotone line 104
  7. theorem OAI.UniqueGames.Foundations.Repetition.SelectionSequence.selectedSet_univ line 110
  8. theorem OAI.UniqueGames.Foundations.Repetition.SelectionSequence.selectedSet_step line 117
  9. def OAI.UniqueGames.Foundations.Repetition.SelectionSequence.SetStep line 132
  10. theorem OAI.UniqueGames.Foundations.Repetition.SelectionSequence.totalSetStep line 138
  11. theorem OAI.UniqueGames.Foundations.Repetition.SelectionSequence.exists_scalar_sequence line 153
  12. def OAI.UniqueGames.Foundations.Repetition.SelectionSequence.ConditionalCoordinateBound line 188
  13. theorem OAI.UniqueGames.Foundations.Repetition.SelectionSequence.repetition_success_le_of_conditionalCoordinateBound line 200