OAI/Computability/DegreeRigidity/CohenForcing/CohenConditionCode.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TuringRigidity.CohenConditionCode.graphline 12 - theorem
OAI.TuringRigidity.CohenConditionCode.pair_mem_graphline 16 - theorem
OAI.TuringRigidity.CohenConditionCode.mem_graphline 36 - theorem
OAI.TuringRigidity.CohenConditionCode.graph_subset_iffline 44 - theorem
OAI.TuringRigidity.CohenConditionCode.graph_injectiveline 52 - def
OAI.TuringRigidity.CohenConditionCode.SingleValuedline 58 - def
OAI.TuringRigidity.CohenConditionCode.IsConditionline 62 - theorem
OAI.TuringRigidity.CohenConditionCode.graph_isConditionline 65 - theorem
OAI.TuringRigidity.CohenConditionCode.isCondition_iff_graphline 82