OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainPrefixPriorFields.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.GroundMainPrefix.serialFieldUnion line 17
2. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.serialFieldUnion_ground line 20
3. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.serialFieldUnion_rank_le_code line 24
4. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.serialFieldUnion_mem line 28
5. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.historyFieldValue_transition line 32
6. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.historyFieldValue_compatible line 39
7. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.serialFieldGraph_entry line 47
8. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.serialFieldUnion_entry line 71
9. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.serialFieldUnion_at line 78
10. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.serialFieldUnion_function line 89
11. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.serialFieldUnion_restrict line 101
12. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPriorFields line 117
13. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPriorFields_graph line 121
14. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPriorFields_values line 124
15. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPriorFields_bound_rank_le_code line 129
16. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPriorFields_code_ground line 139
17. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPriorFields_code_rank_lt line 142