OAI/Computability/DegreeRigidity/OrdinalCodes/OrdinalSumSets.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.OrdinalArithmetic.leftNode line 9
  2. def OAI.TuringRigidity.OrdinalArithmetic.rightNode line 10
  3. theorem OAI.TuringRigidity.OrdinalArithmetic.leftNode_inj line 12
  4. theorem OAI.TuringRigidity.OrdinalArithmetic.rightNode_inj line 15
  5. theorem OAI.TuringRigidity.OrdinalArithmetic.leftNode_ne_rightNode line 18
  6. def OAI.TuringRigidity.OrdinalArithmetic.sumDomain line 25
  7. theorem OAI.TuringRigidity.OrdinalArithmetic.mem_sumDomain line 28
  8. def OAI.TuringRigidity.OrdinalArithmetic.SumLess line 33
  9. def OAI.TuringRigidity.OrdinalArithmetic.sumRelation line 38
  10. theorem OAI.TuringRigidity.OrdinalArithmetic.sumRelation_on line 42
  11. theorem OAI.TuringRigidity.OrdinalArithmetic.pair_mem_sumRelation line 45
  12. def OAI.TuringRigidity.OrdinalArithmetic.taggedClause line 56
  13. theorem OAI.TuringRigidity.OrdinalArithmetic.taggedClause_eval line 62
  14. def OAI.TuringRigidity.OrdinalArithmetic.sumLessFormula line 68
  15. theorem OAI.TuringRigidity.OrdinalArithmetic.sumLessFormula_eval line 72
  16. def OAI.TuringRigidity.OrdinalArithmetic.sumRelationFormula line 77
  17. theorem OAI.TuringRigidity.OrdinalArithmetic.sumRelationFormula_eval line 81
  18. theorem OAI.TuringRigidity.OrdinalArithmetic.sumDomain_mem line 95
  19. theorem OAI.TuringRigidity.OrdinalArithmetic.sumRelation_mem line 104