OAI/Computability/DegreeRigidity/SetModels/IdealInterpretation.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.TuringRigidity.IdealInterpretation.DegreeIdeal line 8
  2. structure OAI.TuringRigidity.IdealInterpretation.Element line 14
  3. instance OAI.TuringRigidity.IdealInterpretation.(instance at line 18) line 18
  4. theorem OAI.TuringRigidity.IdealInterpretation.Element.ext line 20
  5. instance OAI.TuringRigidity.IdealInterpretation.(instance at line 23) line 23
  6. instance OAI.TuringRigidity.IdealInterpretation.(instance at line 26) line 26
  7. instance OAI.TuringRigidity.IdealInterpretation.(instance at line 42) line 42
  8. theorem OAI.TuringRigidity.IdealInterpretation.coe_sup line 49
  9. theorem OAI.TuringRigidity.IdealInterpretation.coe_bot line 50
  10. theorem OAI.TuringRigidity.IdealInterpretation.coe_finset_sup line 52
  11. def OAI.TuringRigidity.IdealInterpretation.nontrivial line 62
  12. def OAI.TuringRigidity.IdealInterpretation.antichain line 65
  13. theorem OAI.TuringRigidity.IdealInterpretation.map_nontrivial line 68
  14. theorem OAI.TuringRigidity.IdealInterpretation.map_antichain line 79
  15. theorem OAI.TuringRigidity.IdealInterpretation.ideal_nontrivial line 93
  16. theorem OAI.TuringRigidity.IdealInterpretation.ideal_antichain line 101
  17. theorem OAI.TuringRigidity.IdealInterpretation.transport_antichain line 112
  18. structure OAI.TuringRigidity.IdealInterpretation.ACode line 117
  19. def OAI.TuringRigidity.IdealInterpretation.ACode.external line 122
  20. def OAI.TuringRigidity.IdealInterpretation.ACode.map line 123
  21. theorem OAI.TuringRigidity.IdealInterpretation.ACode.transport line 125
  22. structure OAI.TuringRigidity.IdealInterpretation.SCode line 129
  23. def OAI.TuringRigidity.IdealInterpretation.SCode.external line 134
  24. def OAI.TuringRigidity.IdealInterpretation.SCode.map line 135
  25. theorem OAI.TuringRigidity.IdealInterpretation.SCode.transport line 138
  26. structure OAI.TuringRigidity.IdealInterpretation.RCode line 145
  27. def OAI.TuringRigidity.IdealInterpretation.RCode.external line 149
  28. def OAI.TuringRigidity.IdealInterpretation.RCode.map line 151
  29. theorem OAI.TuringRigidity.IdealInterpretation.RCode.internal line 154
  30. theorem OAI.TuringRigidity.IdealInterpretation.map_sup_finset line 167
  31. theorem OAI.TuringRigidity.IdealInterpretation.RCode.transport line 174