OAI/SetTheory/PartitionPrinciple/Geometry/StructuralPreparationSourceImages.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rawStageRefinementAssignmentActionGraph_branch_bound line 10
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_structuralAssignments line 22
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignment_branch_unique line 44
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentActionGraph_branch_entry line 63
  5. def OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentImage line 98
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentImage_subset line 101
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentImage_mono line 105
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentImage_one line 120
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentImage_mul line 125
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentLevels_entry line 140
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignments_cut_eq line 170
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignments_mono line 188
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignments_history_restrict line 196
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentSection_mem line 228
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentImage_mem line 240
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentImage_small line 251
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentActionGraph_history_restrict line 278
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentActionGraph_prefix_entry line 292
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentActionGraph_domain_restrict line 323
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentSection_entry line 342
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentSection_domain_restrict line 359
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentActionGraph_earlier_iff line 384
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentImage_entry line 415
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentImage_history_restrict line 427
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentImage_branch line 433
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentImage_domain_restrict line 457
  27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentImage_cut line 476
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentImage_prefix_cut line 504
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentActionGraph_branch_iff line 528
  30. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentImage_select_branch line 552
  31. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentImage_target_branch_iff line 591
  32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentImage_rawTests_branch_iff line 612
  33. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentImage_decode line 646
  34. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignmentImage_selected_edge line 718