OAI/SetTheory/PartitionPrinciple/Forcing/GroundNiceRefinementIndexActionLaws.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndex_act_iff line 23
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndex_fixed line 67
  3. def OAI.PartitionPilot.Forcing.TransitiveGround.stageOneNameAction line 101
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneNameAction_val line 105
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneNameAction_one line 109
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneNameAction_mul line 113
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneNameAction_forces_iff line 119
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneNameAction_class line 133
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneNameAction_map line 142
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneNameAction_visibility line 155
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneActivity_act_iff line 187
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneProfile_act_iff line 200
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneCompatibility_act_iff line 216
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneCollisionTest_act_iff line 233
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneSingleTests_act_iff line 253
  16. def OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndexCoordinateGraphs line 288
  17. def OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndexActionGraph line 297
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_niceRefinementIndexActionGraph line 303
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndexActionGraph_mem line 314
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndexActionGraph_entry line 345
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndexActionGraph_function line 405
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.inverse_edge line 450
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndexActionGraph_inverse_iff line 471
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndexActionGraph_injection line 480