OAI/SetTheory/PartitionPrinciple/Geometry/TaskSystem.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Compression.RecursiveMaps.meetEmbedding_ext line 13
  2. theorem OAI.PartitionPilot.Compression.RecursiveMaps.meetFilter_ext line 24
  3. theorem OAI.PartitionPilot.Compression.RecursiveMaps.pushFilter_iso_image line 34
  4. def OAI.PartitionPilot.Compression.RecursiveMaps.identityIso line 48
  5. def OAI.PartitionPilot.Compression.RecursiveMaps.composeIso line 52
  6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.pushFilter_comp line 62
  7. structure OAI.PartitionPilot.Compression.RecursiveMaps.TaskDatum line 74
  8. structure OAI.PartitionPilot.Compression.RecursiveMaps.TaskDatum.Geometry line 86
  9. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskDatum.transform line 93
  10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskDatum.transform_identity line 101
  11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskDatum.transform_composition line 111
  12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskDatum.geometry_transform line 121
  13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskDatum.transform_ext line 139
  14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskDatum.transform_agrees line 153
  15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskDatum.permutations_agree line 168
  16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskDatum.representatives_compatible line 180
  17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskDatum.successor_agreement line 192
  18. structure OAI.PartitionPilot.Compression.RecursiveMaps.GroupData line 228
  19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.transform_congr line 238
  20. structure OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem line 250
  21. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.perm line 270
  22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.transport line 272
  23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.perm_one line 276
  24. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.perm_mul line 282
  25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.perm_left line 289
  26. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.perm_right line 292
  27. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.action_left line 295
  28. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.action_right line 299
  29. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.source_invariant line 303
  30. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.representative line 308
  31. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.represents line 310
  32. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.base_top line 314
  33. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.representative_target line 322
  34. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.ground_compatible line 326
  35. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.positive_perms_agree line 333
  36. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.initial line 339
  37. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.filter_covariant line 352