OAI/Computability/DegreeRigidity/SetModels/InternalCollapseConditions.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.Prefix line 11
  2. theorem OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.prefix_subset line 14
  3. theorem OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.prefix_empty line 21
  4. def OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.append line 24
  5. theorem OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.mem_append line 27
  6. theorem OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.append_function line 31
  7. theorem OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.append_mem line 61
  8. def OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.prefixFormula line 67
  9. theorem OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.eval_prefixFormula line 69
  10. theorem OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.conditions_exist line 76
  11. def OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.order line 90
  12. def OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.collapsePreorder line 99
  13. def OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.top line 105
  14. def OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.orderSet line 113
  15. theorem OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.orderSet_mem line 116
  16. theorem OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.orderSet_pair line 124