OAI/Computability/PerfectCompleteness/Foundations/ReducedDomains.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.ReducedDomains.Allowed line 13
  2. theorem OAI.PerfectCompleteness.ReducedDomains.allowed_nonempty line 19
  3. theorem OAI.PerfectCompleteness.ReducedDomains.localReduction_range_iff line 27
  4. theorem OAI.PerfectCompleteness.ReducedDomains.localReduction_allowed line 72
  5. def OAI.PerfectCompleteness.ReducedDomains.legalAssignments line 77
  6. theorem OAI.PerfectCompleteness.ReducedDomains.mem_legalAssignments line 80
  7. theorem OAI.PerfectCompleteness.ReducedDomains.legalAssignments_nonempty line 83
  8. theorem OAI.PerfectCompleteness.ReducedDomains.range_reduction line 89
  9. def OAI.PerfectCompleteness.ReducedDomains.valueCode line 112
  10. theorem OAI.PerfectCompleteness.ReducedDomains.valueCode_injective line 117
  11. theorem OAI.PerfectCompleteness.ReducedDomains.reducedValue_finite line 121
  12. theorem OAI.PerfectCompleteness.ReducedDomains.legalAssignments_finite line 124