OAI/SetTheory/PartitionPrinciple/Geometry/GroundCodedBinaryHeights.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PartitionPilot.Forcing.StrictHeightGraphCode line 15
2. theorem OAI.PartitionPilot.Forcing.StrictLexHeightCode.strictHeightGraph line 20
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundHeightInterpolation line 34
4. def OAI.PartitionPilot.Forcing.lexProductOrder line 115
5. theorem OAI.PartitionPilot.Forcing.mem_lexProductOrder line 121
6. theorem OAI.PartitionPilot.Forcing.pair_mem_lexProductOrder line 133
7. theorem OAI.PartitionPilot.Forcing.lexProductOrder_code line 146
8. def OAI.PartitionPilot.Forcing.BoundedFormula.lexProductEntryFormula line 189
9. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_lexProductEntryFormula line 195
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.lexProductOrder_mem line 210
11. def OAI.PartitionPilot.Forcing.StrictLinearOrderCode.smallOrder line 242
12. def OAI.PartitionPilot.Forcing.StrictHeightGraphCode.smallHeight line 250
13. theorem OAI.PartitionPilot.Forcing.StrictHeightGraphCode.smallHeight_graph line 260
14. theorem OAI.PartitionPilot.SetRealization.Presentation.strictHeightGraphCode line 273
15. theorem OAI.PartitionPilot.SetRealization.Presentation.lexProductOrder_iff line 290
16. theorem OAI.PartitionPilot.SetRealization.Presentation.compose_graphs line 302
17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.composed_graph_mem line 337
18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.paired_graph_mem line 344
19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.binaryTuple_ground line 373
20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rectangleTuple_ground line 415
21. structure OAI.PartitionPilot.Forcing.IntervalHeightCode line 468
22. theorem OAI.PartitionPilot.Forcing.StrictHeightGraphCode.weak line 472
23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_binaryTileIntervalHeight line 505
24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_rectangleTileIntervalHeight line 528
25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_requestTileIntervalHeight line 585
26. def OAI.PartitionPilot.Forcing.intervalHeightCandidate line 618
27. def OAI.PartitionPilot.Forcing.intervalHeightRelation line 622
28. theorem OAI.PartitionPilot.Forcing.pair_mem_intervalHeightRelation line 626
29. theorem OAI.PartitionPilot.Forcing.intervalHeightCandidate_iff line 637
30. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_codedBinaryTileHeight line 675
31. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_separationTileHeight line 709
32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_compressionTileHeight line 727