OAI/Computability/DegreeRigidity/OrdinalCodes/OmegaModelCore.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.TuringRigidity.OmegaModelCore.OmegaData line 9
2. def OAI.TuringRigidity.OmegaModelCore.OmegaData.power line 21
3. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.mem_power line 23
4. def OAI.TuringRigidity.OmegaModelCore.OmegaData.level line 26
5. def OAI.TuringRigidity.OmegaModelCore.OmegaData.InCore line 30
6. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.num_accessible line 32
7. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.level_accessible line 40
8. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.core_accessible line 52
9. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.core_transitive line 56
10. abbrev OAI.TuringRigidity.OmegaModelCore.OmegaData.Core line 65
11. def OAI.TuringRigidity.OmegaModelCore.OmegaData.Rel line 66
12. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.core_wellFounded line 68
13. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.core_extensional line 78
14. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.core_is_wellFounded_extensional line 88