OAI/SetTheory/PartitionPrinciple/Forcing/RecursiveAction.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Compression.RecursiveMaps.isoOfOrder line 13
  2. def OAI.PartitionPilot.Compression.RecursiveMaps.inverseIso line 38
  3. structure OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry line 46
  4. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.symm line 63
  5. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.renameLabel line 78
  6. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.renameFresh line 83
  7. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.act line 86
  8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.fresh_task_eq line 91
  9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.rename_left line 99
  10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.rename_right line 105
  11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.act_left line 111
  12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.act_right line 117
  13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.shadow_covariant line 123
  14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.upper_covariant line 130
  15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.inside_forward line 145
  16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.inside_iff line 153
  17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.act_order line 163
  18. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.nextIso line 182
  19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.nextIso_old line 185
  20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.nextIso_fresh line 188
  21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.nextIso_meet line 191
  22. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.identity line 196
  23. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.comp line 206
  24. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.next_identity line 225
  25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.next_composition line 229
  26. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.next_inverse line 234
  27. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.lift_equivariant line 238
  28. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.fresh_positive line 256
  29. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSymmetry.agreement_persists line 277
  30. def OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.nextInputs line 304
  31. def OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.nextSymmetry line 315