OAI/Computability/DegreeRigidity/SetModels/InternalInfinity.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.BoundedSetTheory.natSet line 10
  2. theorem OAI.TuringRigidity.BoundedSetTheory.natSet_eq_mk line 14
  3. theorem OAI.TuringRigidity.BoundedSetTheory.mem_natSet line 19
  4. theorem OAI.TuringRigidity.BoundedSetTheory.natSet_injective line 34
  5. theorem OAI.TuringRigidity.BoundedSetTheory.natSet_mem_natSet line 43
  6. theorem OAI.TuringRigidity.BoundedSetTheory.natSet_transitive line 47
  7. theorem OAI.TuringRigidity.BoundedSetTheory.mem_omega line 53
  8. theorem OAI.TuringRigidity.BoundedSetTheory.omega_transitive line 63
  9. def OAI.TuringRigidity.BoundedSetTheory.Formula.empty line 70
  10. def OAI.TuringRigidity.BoundedSetTheory.Formula.successor line 71
  11. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_empty line 75
  12. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_successor line 82
  13. def OAI.TuringRigidity.BoundedSetTheory.Formula.zeroOrSuccessor line 95
  14. def OAI.TuringRigidity.BoundedSetTheory.Formula.finiteOrdinal line 98
  15. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_zeroOrSuccessor line 102
  16. def OAI.TuringRigidity.BoundedSetTheory.FiniteOrdinal line 107
  17. theorem OAI.TuringRigidity.BoundedSetTheory.eval_finiteOrdinal line 111
  18. theorem OAI.TuringRigidity.BoundedSetTheory.finiteOrdinal_natSet line 116
  19. theorem OAI.TuringRigidity.BoundedSetTheory.finiteOrdinal_iff line 129
  20. def OAI.TuringRigidity.BoundedSetTheory.Infinity line 143
  21. theorem OAI.TuringRigidity.BoundedSetTheory.omega_mem line 148