OAI/Computability/DegreeRigidity/SetModels/RecursiveNameSymmetry.lean
13 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.TuringRigidity.RecursiveNames.val_mapFilterline 11 - theorem
OAI.TuringRigidity.RecursiveNames.extension_mapFilterline 17 - def
OAI.TuringRigidity.RecursiveNames.realsline 30 - theorem
OAI.TuringRigidity.RecursiveNames.reals_mapFilterline 32 - inductive
OAI.TuringRigidity.RecursiveNames.Formulaline 38 - def
OAI.TuringRigidity.RecursiveNames.Formula.Realizeline 45 - theorem
OAI.TuringRigidity.RecursiveNames.realize_mapFilterline 52 - theorem
OAI.TuringRigidity.RecursiveNames.definable_subset_mapFilterline 59 - def
OAI.TuringRigidity.RecursiveNames.extensionSetline 70 - theorem
OAI.TuringRigidity.RecursiveNames.extensionSet_coeline 74 - def
OAI.TuringRigidity.RecursiveNames.definedSetline 83 - theorem
OAI.TuringRigidity.RecursiveNames.mem_definedSetline 87 - theorem
OAI.TuringRigidity.RecursiveNames.definedSet_mapFilterline 92