OAI/SetTheory/PartitionPrinciple/Definability/ExternalColumnCodes.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.successorColumnGraph_injection line 11
2. structure OAI.PartitionPilot.Forcing.ExternalColumnCode line 31
3. theorem OAI.PartitionPilot.Forcing.ExternalColumnCode.value_mem line 43
4. theorem OAI.PartitionPilot.Forcing.ExternalColumnCode.old_below line 46
5. theorem OAI.PartitionPilot.Forcing.ExternalColumnCode.injection line 49
6. def OAI.PartitionPilot.Forcing.ExternalColumnCode.smallColumn line 52
7. theorem OAI.PartitionPilot.Forcing.ExternalColumnCode.smallColumn_graph line 55
8. theorem OAI.PartitionPilot.Forcing.ExternalColumnCode.smallColumn_increasing line 71
9. theorem OAI.PartitionPilot.Forcing.ExternalColumnCode.smallColumn_bounded line 76
10. theorem OAI.PartitionPilot.Forcing.ExternalColumnCode.old_height_below line 79
11. structure OAI.PartitionPilot.Forcing.GroundExternalColumnData line 89