OAI/Computability/DegreeRigidity/CohenForcing/CohenSymmetry.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.TuringRigidity.CohenSymmetry.Condition line 9
  2. instance OAI.TuringRigidity.CohenSymmetry.(instance at line 15) line 15
  3. instance OAI.TuringRigidity.CohenSymmetry.(instance at line 29) line 29
  4. def OAI.TuringRigidity.CohenSymmetry.flip line 33
  5. theorem OAI.TuringRigidity.CohenSymmetry.flip_involutive line 37
  6. theorem OAI.TuringRigidity.CohenSymmetry.flip_mono line 44
  7. def OAI.TuringRigidity.CohenSymmetry.flipIso line 54
  8. def OAI.TuringRigidity.CohenSymmetry.Compatible line 64
  9. def OAI.TuringRigidity.CohenSymmetry.merge line 67
  10. theorem OAI.TuringRigidity.CohenSymmetry.merge_le_left line 75
  11. theorem OAI.TuringRigidity.CohenSymmetry.merge_le_right line 79
  12. def OAI.TuringRigidity.CohenSymmetry.matchingMask line 85
  13. theorem OAI.TuringRigidity.CohenSymmetry.matching_compatible line 88
  14. theorem OAI.TuringRigidity.CohenSymmetry.homogeneous line 95
  15. def OAI.TuringRigidity.CohenSymmetry.tailIso line 100
  16. theorem OAI.TuringRigidity.CohenSymmetry.remove_tail line 108
  17. theorem OAI.TuringRigidity.CohenSymmetry.top_weak_of_invariant line 120
  18. theorem OAI.TuringRigidity.CohenSymmetry.remove_tail_weak line 129
  19. theorem OAI.TuringRigidity.CohenSymmetry.top_weak_of_weak_invariant line 147