OAI/Computability/DegreeRigidity/OrdinalCodes/LevelOrdinalHeight.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TuringRigidity.RelativeConstructible.ordinalHeight_level line 9
2. theorem OAI.TuringRigidity.RelativeConstructible.ordinal_mem_level_iff line 30
3. theorem OAI.TuringRigidity.RelativeConstructible.largest_ordinal_level_succ line 34
4. theorem OAI.TuringRigidity.RelativeConstructible.largest_ordinal_at_difference line 42