OAI/Computability/PerfectCompleteness/Construction/FlexibleLocalCompletionLemmas.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PerfectCompleteness.FlexibleLocalCompletion.Compatible line 20
  2. def OAI.PerfectCompleteness.FlexibleLocalCompletion.localLegalEquiv line 28
  3. theorem OAI.PerfectCompleteness.FlexibleLocalCompletion.localLegalEquiv_apply_val line 33
  4. theorem OAI.PerfectCompleteness.FlexibleLocalCompletion.card_legal line 37
  5. theorem OAI.PerfectCompleteness.FlexibleLocalCompletion.input_admissible line 43
  6. def OAI.PerfectCompleteness.FlexibleLocalCompletion.result line 62
  7. theorem OAI.PerfectCompleteness.FlexibleLocalCompletion.result_correct line 66
  8. def OAI.PerfectCompleteness.FlexibleLocalCompletion.family line 72
  9. theorem OAI.PerfectCompleteness.FlexibleLocalCompletion.family_size line 95
  10. theorem OAI.PerfectCompleteness.FlexibleLocalCompletion.family_map line 100
  11. theorem OAI.PerfectCompleteness.FlexibleLocalCompletion.family_size_le line 105
  12. def OAI.PerfectCompleteness.LocalCompletionGame.input line 129
  13. theorem OAI.PerfectCompleteness.LocalCompletionGame.input_mask_true line 134
  14. theorem OAI.PerfectCompleteness.LocalCompletionGame.input_image_legal line 139
  15. def OAI.PerfectCompleteness.LocalCompletionGame.localLegalEquiv line 144
  16. theorem OAI.PerfectCompleteness.LocalCompletionGame.localLegalEquiv_apply_val line 157
  17. theorem OAI.PerfectCompleteness.LocalCompletionGame.card_legal line 160
  18. theorem OAI.PerfectCompleteness.LocalCompletionGame.input_admissible line 165
  19. def OAI.PerfectCompleteness.LocalCompletionGame.result line 185
  20. theorem OAI.PerfectCompleteness.LocalCompletionGame.result_correct line 188
  21. def OAI.PerfectCompleteness.LocalCompletionGame.family line 195
  22. theorem OAI.PerfectCompleteness.LocalCompletionGame.family_size line 217
  23. theorem OAI.PerfectCompleteness.LocalCompletionGame.family_map line 223
  24. theorem OAI.PerfectCompleteness.LocalCompletionGame.family_size_le line 229