OAI/Computability/DegreeRigidity/Representation/RealGeneratedPart.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.RealGeneratedPart.tagLower line 12
  2. def OAI.TuringRigidity.RealGeneratedPart.bit line 16
  3. def OAI.TuringRigidity.RealGeneratedPart.part line 19
  4. theorem OAI.TuringRigidity.RealGeneratedPart.bit_mem_part line 22
  5. theorem OAI.TuringRigidity.RealGeneratedPart.part_compl line 25
  6. def OAI.TuringRigidity.RealGeneratedPart.projection line 28
  7. def OAI.TuringRigidity.RealGeneratedPart.decision line 31
  8. theorem OAI.TuringRigidity.RealGeneratedPart.decision_dense line 34
  9. def OAI.TuringRigidity.RealGeneratedPart.value line 42
  10. theorem OAI.TuringRigidity.RealGeneratedPart.bit_hit_iff line 45
  11. theorem OAI.TuringRigidity.RealGeneratedPart.projected_bit_iff line 61
  12. theorem OAI.TuringRigidity.RealGeneratedPart.same_real_generators line 79
  13. theorem OAI.TuringRigidity.RealGeneratedPart.projected_countable_presentation line 90