OAI/SetTheory/PartitionPrinciple/Transfinite/GroundOrdinalOrderCodes.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.ordinalImageOrder line 10
2. theorem OAI.PartitionPilot.Forcing.ordinalImageOrder_subset line 15
3. theorem OAI.PartitionPilot.Forcing.mem_ordinalImageOrder line 18
4. theorem OAI.PartitionPilot.Forcing.pair_mem_ordinalImageOrder line 26
5. structure OAI.PartitionPilot.Forcing.OrdinalOrderCode line 39
6. theorem OAI.PartitionPilot.Forcing.ordinalImageOrder_code line 46
7. theorem OAI.PartitionPilot.Forcing.OrdinalOrderCode.eq_image line 51
8. theorem OAI.PartitionPilot.Forcing.OrdinalOrderCode.predecessor_exists line 73
9. theorem OAI.PartitionPilot.Forcing.OrdinalOrderCode.matched_value_unique line 93
10. theorem OAI.PartitionPilot.Forcing.OrdinalOrderCode.domain_unique line 111
11. theorem OAI.PartitionPilot.Forcing.ordinalImageOrder_domain_unique line 134
12. def OAI.PartitionPilot.Forcing.BoundedFormula.ordinalImagePairFormula line 152
13. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_ordinalImagePairFormula line 156
14. def OAI.PartitionPilot.Forcing.BoundedFormula.ordinalImageEntryFormula line 163
15. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_ordinalImageEntryFormula line 167
16. def OAI.PartitionPilot.Forcing.BoundedFormula.ordinalImageFormula line 174
17. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_ordinalImageFormula line 179
18. def OAI.PartitionPilot.Forcing.SetFormula.ordinalImageWitnessFormula line 207
19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinalImageOrder_mem line 220
20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_ordinalImageWitnessFormula line 240