OAI/Computability/DegreeRigidity/CohenForcing/InternalCohenConditions.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.InternalCohen.bitSet line 9
  2. def OAI.TuringRigidity.InternalCohen.alphabet line 11
  3. theorem OAI.TuringRigidity.InternalCohen.bitSet_injective line 13
  4. theorem OAI.TuringRigidity.InternalCohen.mem_alphabet line 18
  5. def OAI.TuringRigidity.InternalCohen.wordCode line 26
  6. theorem OAI.TuringRigidity.InternalCohen.mem_wordCode line 29
  7. theorem OAI.TuringRigidity.InternalCohen.pair_mem_wordCode line 33
  8. theorem OAI.TuringRigidity.InternalCohen.wordCode_function line 44
  9. theorem OAI.TuringRigidity.InternalCohen.wordCode_subset_iff line 61
  10. theorem OAI.TuringRigidity.InternalCohen.wordCode_injective line 78
  11. theorem OAI.TuringRigidity.InternalCohen.prefix_iff_wordCode line 84
  12. def OAI.TuringRigidity.InternalCohen.conditions line 108
  13. theorem OAI.TuringRigidity.InternalCohen.mem_conditions line 111
  14. theorem OAI.TuringRigidity.InternalCohen.alphabet_mem line 115
  15. theorem OAI.TuringRigidity.InternalCohen.conditions_mem line 120
  16. def OAI.TuringRigidity.InternalCohen.encodeCondition line 129
  17. theorem OAI.TuringRigidity.InternalCohen.label_encodeCondition line 132
  18. def OAI.TuringRigidity.InternalCohen.conditionEquiv line 135