OAI/Computability/DegreeRigidity/SetModels/NameUnionCode.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.TransitiveNameModel.iterUnion line 9
  2. theorem OAI.TuringRigidity.TransitiveNameModel.iterUnion_mem line 13
  3. theorem OAI.TuringRigidity.TransitiveNameModel.first_mem_doubleUnion line 20
  4. theorem OAI.TuringRigidity.TransitiveNameModel.iterUnion_lift line 27
  5. theorem OAI.TuringRigidity.TransitiveNameModel.iterUnion_add line 36
  6. theorem OAI.TuringRigidity.TransitiveNameModel.second_child_bound line 42
  7. theorem OAI.TuringRigidity.TransitiveNameModel.label_surjective line 49
  8. theorem OAI.TuringRigidity.TransitiveNameModel.pair_mem_encode line 53
  9. def OAI.TuringRigidity.TransitiveNameModel.unionPredicate line 64
  10. def OAI.TuringRigidity.TransitiveNameModel.unionFormula line 70
  11. theorem OAI.TuringRigidity.TransitiveNameModel.eval_unionFormula line 77
  12. def OAI.TuringRigidity.TransitiveNameModel.unionCode line 83
  13. theorem OAI.TuringRigidity.TransitiveNameModel.mem_unionCode line 86
  14. theorem OAI.TuringRigidity.TransitiveNameModel.unionCode_mem line 96
  15. theorem OAI.TuringRigidity.TransitiveNameModel.encode_union line 116