OAI/SetTheory/PartitionPrinciple/Transfinite/GroundRecursiveRowCompleteProjection.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementDataHistory.greatest line 14
2. def OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryPartialOrder line 27
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryDecodedOrder_eq line 31
4. def OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryOrderTop line 37
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryDecodedTop_eq line 47
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryRowNameFamily_power_eq line 72
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryRowNameFamily_square_eq line 90
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.recursiveRefinementStageSystem line 116
9. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.splice_mem line 204
10. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.splice_lifting line 219
11. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.cut_mem_le line 252
12. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.cut_order_le line 271
13. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.include_mem line 283
14. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.restrictionGraph_function line 330
15. def OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.restrictionFunction line 338
16. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.restrictionFunction_raw line 342
17. def OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.restriction line 353
18. def OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.inclusionFunction line 397
19. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.inclusionFunction_raw line 408
20. def OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.inclusion line 411
21. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.restrictionFunction_graph line 456
22. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.restrictionFunction_graph_mem line 468
23. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.inclusionFunction_graph line 486
24. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.inclusionFunction_graph_mem line 504
25. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.completeProjection line 539
26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowCarrier_shape line 621
27. def OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryRowFunction line 628
28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryRowFunction_code line 632
29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryRowFunction_coordinates line 643
30. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryRowFunction_graph line 651
31. def OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryRowRestriction line 658
32. def OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryRowEmbedding line 676
33. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryRow_retract line 701
34. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryRow_le_include line 705
35. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryRowInclusion_graph line 727
36. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryRowGraphs_mem line 741
37. theorem OAI.PartitionPilot.Forcing.TransitiveGround.assignmentCut_zero line 754
38. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryRow_completeProjection line 759