OAI/SetTheory/PartitionPrinciple/Geometry/MainRectangles.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Compression.RecursiveMaps.groupDataOfGroup line 12
  2. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.Eligible line 25
  3. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.AllTasks line 28
  4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.eligible_transform line 30
  5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.eligible_source_proper line 39
  6. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.allTaskSystem line 53
  7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.allTaskSystem_complete line 68
  8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.allTaskSystem_literal line 72
  9. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.labelledTask line 77
  10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.labelledTask_label line 82
  11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.labelledTask_injective line 85
  12. structure OAI.PartitionPilot.Compression.RecursiveMaps.ActionRectangle line 98
  13. def OAI.PartitionPilot.Compression.RecursiveMaps.ActionRectangle.toInput line 113
  14. def OAI.PartitionPilot.Compression.RecursiveMaps.CompressionAlgebra.liftRectangle line 133