OAI/SetTheory/PartitionPrinciple/Forcing/InitialAction.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initialFreshEq line 15
  2. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initialRename line 21
  3. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initialAct line 27
  4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initialRename_left line 31
  5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initialRename_right line 36
  6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initialAct_left line 41
  7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initialAct_right line 47
  8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initialShadow line 53
  9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initialInside_forward line 63
  10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initialInside_iff line 72
  11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initialOrder line 82
  12. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initialIso line 102
  13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initialIso_old line 106
  14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initialIso_one line 109
  15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initialIso_mul line 117
  16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initial_equivariant line 126
  17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initial_agreement line 140
  18. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initialInputs line 150
  19. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initialSymmetry line 156
  20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initial_negative line 165