OAI/Computability/PerfectCompleteness/Foundations/KeyFiniteness.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CanonicalKeys.KeyLabel line 17
  2. instance OAI.PerfectCompleteness.CanonicalKeys.KeyLabel_finite line 19
  3. instance OAI.PerfectCompleteness.CanonicalKeys.keyLabel_nonempty line 23
  4. theorem OAI.PerfectCompleteness.CanonicalKeys.label_finite line 28
  5. theorem OAI.PerfectCompleteness.CanonicalKeys.label_nonempty line 32
  6. theorem OAI.PerfectCompleteness.CanonicalKeys.card_label_le_output line 36
  7. theorem OAI.PerfectCompleteness.CanonicalKeys.card_label_le_assignment line 40
  8. def OAI.PerfectCompleteness.CanonicalKeys.answerEquivFinSeven line 44
  9. theorem OAI.PerfectCompleteness.CanonicalKeys.card_answer line 55
  10. theorem OAI.PerfectCompleteness.CanonicalKeys.card_slotDomain_le_seven line 58
  11. theorem OAI.PerfectCompleteness.CanonicalKeys.card_assignment_le_seven_pow line 65
  12. theorem OAI.PerfectCompleteness.CanonicalKeys.card_label_le_seven_pow line 74
  13. theorem OAI.PerfectCompleteness.CanonicalKeys.card_keyLabel_le_output line 78
  14. theorem OAI.PerfectCompleteness.CanonicalKeys.card_keyLabel_le_seven_pow line 82