OAI/Computability/DegreeRigidity/Syntax/BoundedDecoding.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.BoundedDecoding.AntichainBelow line 8
  2. def OAI.TuringRigidity.BoundedDecoding.LocalNontrivial line 11
  3. def OAI.TuringRigidity.BoundedDecoding.LocalAntichain line 14
  4. theorem OAI.TuringRigidity.BoundedDecoding.local_nontrivial_iff line 19
  5. theorem OAI.TuringRigidity.BoundedDecoding.local_antichain_iff line 27
  6. def OAI.TuringRigidity.BoundedDecoding.SetBelow line 37
  7. def OAI.TuringRigidity.BoundedDecoding.LocalGraph line 40
  8. def OAI.TuringRigidity.BoundedDecoding.LocalSet line 43
  9. theorem OAI.TuringRigidity.BoundedDecoding.local_graph_iff line 46
  10. theorem OAI.TuringRigidity.BoundedDecoding.graph_bounded line 51
  11. theorem OAI.TuringRigidity.BoundedDecoding.local_set_iff line 55
  12. def OAI.TuringRigidity.BoundedDecoding.RelationBelow line 60
  13. def OAI.TuringRigidity.BoundedDecoding.LocalRelation line 63
  14. theorem OAI.TuringRigidity.BoundedDecoding.local_relation_iff line 67