OAI/Computability/DegreeRigidity/CohenForcing/SparseCohenRealName.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.TuringRigidity.SparseCohenRealName.posetline 13 - def
OAI.TuringRigidity.SparseCohenRealName.realNameline 15 - def
OAI.TuringRigidity.SparseCohenRealName.realNameCodeline 20 - theorem
OAI.TuringRigidity.SparseCohenRealName.mem_realNameCodeline 25 - theorem
OAI.TuringRigidity.SparseCohenRealName.realNameCode_memline 35 - theorem
OAI.TuringRigidity.SparseCohenRealName.encode_realNameline 52 - theorem
OAI.TuringRigidity.SparseCohenRealName.realName_internalline 72