OAI/SetTheory/PartitionPrinciple/Forcing/GroundRawRowAssignmentActions.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_rowAssignmentActionGraph line 15
  2. def OAI.PartitionPilot.Forcing.TransitiveGround.rowAssignmentActionOutputFormula line 59
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_rowAssignmentActionOutputFormula line 64
  4. def OAI.PartitionPilot.Forcing.rawActionSection line 83
  5. theorem OAI.PartitionPilot.Forcing.mem_rawActionSection line 87
  6. def OAI.PartitionPilot.Forcing.rawActionMapFamily line 99
  7. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_rawActionSection line 109
  8. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_rawActionMapFamily line 131
  9. theorem OAI.PartitionPilot.Forcing.rawActionSection_eq line 140
  10. theorem OAI.PartitionPilot.Forcing.rawActionMapFamily_eq line 147
  11. theorem OAI.PartitionPilot.Forcing.pair_mem_rawActionMapFamily line 171
  12. theorem OAI.PartitionPilot.Forcing.pair_mem_rawActionSection line 183
  13. def OAI.PartitionPilot.Forcing.rawRowAssignmentActionGraph line 194
  14. theorem OAI.PartitionPilot.Forcing.pair_mem_rawRowAssignmentActionGraph line 199
  15. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_rawRowAssignmentActionGraph line 230
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rawRowAssignmentActionGraph_mem line 241