OAI/Computability/DegreeRigidity/Effective/SetCoding.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- structure
OAI.TuringRigidity.SetCoding.AntichainCodeline 10 - def
OAI.TuringRigidity.SetCoding.AntichainCode.Holdsline 15 - theorem
OAI.TuringRigidity.SetCoding.exists_antichainCodeline 18 - structure
OAI.TuringRigidity.SetCoding.SetCodeline 25 - def
OAI.TuringRigidity.SetCoding.SetCode.Graphline 30 - def
OAI.TuringRigidity.SetCoding.SetCode.Holdsline 33 - theorem
OAI.TuringRigidity.SetCoding.codes_with_tagsline 35 - theorem
OAI.TuringRigidity.SetCoding.countable_set_codingline 83