OAI/Computability/DegreeRigidity/OrdinalCodes/OmegaPowerDefinability.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.TuringRigidity.OrdinalArithmetic.omegaStageStep_exactline 10 - theorem
OAI.TuringRigidity.OrdinalArithmetic.omegaPower_sigmaDefinableline 26 - theorem
OAI.TuringRigidity.OrdinalArithmetic.uniform_omega_powerline 57 - theorem
OAI.TuringRigidity.OrdinalArithmetic.omega_power_image_internalline 63