OAI/Computability/DegreeRigidity/Effective/AntichainDecoding.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TuringRigidity.AntichainDecoding.Nontrivialline 9 - def
OAI.TuringRigidity.AntichainDecoding.Minimalline 13 - def
OAI.TuringRigidity.AntichainDecoding.Antichainline 16 - theorem
OAI.TuringRigidity.AntichainDecoding.nontrivial_sigmaline 19 - theorem
OAI.TuringRigidity.AntichainDecoding.minimal_piline 33 - theorem
OAI.TuringRigidity.AntichainDecoding.antichain_sigmaline 47 - theorem
OAI.TuringRigidity.AntichainDecoding.nontrivial_iffline 52 - theorem
OAI.TuringRigidity.AntichainDecoding.antichain_iffline 72