OAI/Computability/DegreeRigidity/OrdinalCodes/OmegaModelCollapse.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.OmegaModelCore.OmegaData.collapse line 12
2. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.collapse_eq line 15
3. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.mem_collapse line 19
4. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.collapse_injective line 28
5. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.collapse_mem_iff line 47
6. def OAI.TuringRigidity.OmegaModelCore.OmegaData.collapsedModel line 55
7. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.mem_collapsedModel line 57
8. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.collapsedModel_transitive line 62
9. def OAI.TuringRigidity.OmegaModelCore.OmegaData.numNode line 68
10. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.rel_numNode line 70
11. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.collapse_num line 80
12. def OAI.TuringRigidity.OmegaModelCore.OmegaData.omegaNode line 93
13. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.collapse_omega line 95
14. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.collapsedModel_omega line 107
15. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.collapse_real line 110