OAI/SetTheory/PartitionPrinciple/Definability/GroundSerializedCodeRanks.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.time_rank_le_code line 15
2. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.bound_rank_le_code line 18
3. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.graph_rank_le_code line 21
4. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.value_rank_lt_code line 24
5. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.fieldsCode_rank_le_code line 35
6. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.time_rank_le_code line 38
7. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.fieldGraph_rank_le_code line 41
8. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.fieldValue_rank_lt_code line 45
9. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.layerBound_rank_le_code line 49
10. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.layers_rank_le_code line 52
11. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.layerWitness_rank_lt_code line 55