OAI/Computability/DegreeRigidity/OrdinalCodes/OrdinalSumPresentation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TuringRigidity.OrdinalArithmetic.rightNode_ne_leftNode line 9
  2. theorem OAI.TuringRigidity.OrdinalArithmetic.sumLess_left_left line 14
  3. theorem OAI.TuringRigidity.OrdinalArithmetic.sumLess_left_right line 18
  4. theorem OAI.TuringRigidity.OrdinalArithmetic.sumLess_right_left line 22
  5. theorem OAI.TuringRigidity.OrdinalArithmetic.sumLess_right_right line 26
  6. def OAI.TuringRigidity.OrdinalArithmetic.sumValue line 30
  7. theorem OAI.TuringRigidity.OrdinalArithmetic.sumValue_left line 35
  8. theorem OAI.TuringRigidity.OrdinalArithmetic.sumValue_right line 42
  9. theorem OAI.TuringRigidity.OrdinalArithmetic.sumValue_mem line 50
  10. theorem OAI.TuringRigidity.OrdinalArithmetic.sumValue_surjective line 59
  11. theorem OAI.TuringRigidity.OrdinalArithmetic.sumValue_relation line 72
  12. theorem OAI.TuringRigidity.OrdinalArithmetic.sumRelation_wellFounded line 92
  13. theorem OAI.TuringRigidity.OrdinalArithmetic.sumRelation_transitive line 98
  14. theorem OAI.TuringRigidity.OrdinalArithmetic.sum_orderType line 105
  15. theorem OAI.TuringRigidity.OrdinalArithmetic.ordinal_add_internal line 111