OAI/SetTheory/PartitionPrinciple/Geometry/GroundIdentityInsertionTasks.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.identityIdealGraph line 10
  2. theorem OAI.PartitionPilot.Forcing.pair_mem_identityIdealGraph line 13
  3. theorem OAI.PartitionPilot.Forcing.identityIdealGraph_restrictedAction line 18
  4. theorem OAI.PartitionPilot.Forcing.identityInsertion_eligible line 37
  5. def OAI.PartitionPilot.Forcing.identityInsertionTask line 46
  6. theorem OAI.PartitionPilot.Forcing.identityInsertionTask_injective line 49
  7. def OAI.PartitionPilot.Forcing.identityInsertionTaskGraph line 62
  8. theorem OAI.PartitionPilot.Forcing.pair_mem_identityInsertionTaskGraph line 67
  9. def OAI.PartitionPilot.Forcing.BoundedFormula.identityInsertionGraphEntryFormula line 80
  10. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_identityInsertionGraphEntryFormula line 84
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.identityIdealGraph_mem line 102
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.identityInsertionTask_mem line 107
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.identityInsertionTaskGraph_mem line 118
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.identityInsertionTaskGraph_injection line 139
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.identityInsertionTask_fields line 162