OAI/Computability/DegreeRigidity/OrdinalCodes/OmegaModelCoreClosure.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.OmegaModelCore.OmegaData.TransitiveAt line 10
2. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.omega_transitive line 12
3. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.power_transitive line 18
4. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.level_transitive line 24
5. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.level_succ line 29
6. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.level_mono line 33
7. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.core_of_subset_level line 39
8. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.core_subset line 43
9. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.power_core line 48
10. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.pair_core line 56
11. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.union_core line 66
12. theorem OAI.TuringRigidity.OmegaModelCore.OmegaData.collapse_subset_iff line 74