OAI/Computability/DegreeRigidity/SetModels/ElementaryCollapsePoset.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.TuringRigidity.ElementaryModel.definedSet_univline 13 - theorem
OAI.TuringRigidity.ElementaryModel.collapse_bounded_evalline 18 - def
OAI.TuringRigidity.ElementaryModel.ambientConditionsline 26 - theorem
OAI.TuringRigidity.ElementaryModel.mem_ambientConditionsline 29 - theorem
OAI.TuringRigidity.ElementaryModel.ambientConditions_defline 33 - theorem
OAI.TuringRigidity.ElementaryModel.ambientConditions_mem_hullline 43 - theorem
OAI.TuringRigidity.ElementaryModel.collapse_ambientConditionsline 50 - def
OAI.TuringRigidity.ElementaryModel.orderMemberline 78 - theorem
OAI.TuringRigidity.ElementaryModel.eval_orderMemberline 81 - theorem
OAI.TuringRigidity.ElementaryModel.orderSet_mem_hullline 88 - theorem
OAI.TuringRigidity.ElementaryModel.collapse_orderSetline 98 - theorem
OAI.TuringRigidity.ElementaryModel.collapse_selected_conditionline 117