OAI/SetTheory/PartitionPrinciple/Transfinite/CoherentTower.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PartitionPilot.Compression.RecursiveMaps.CompressionStage line 13
  2. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompressionStage.compatible line 47
  3. def OAI.PartitionPilot.Compression.RecursiveMaps.CompressionStage.nextInputs line 64
  4. def OAI.PartitionPilot.Compression.RecursiveMaps.CompressionStage.nextAction line 67
  5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompressionStage.next_action_one line 71
  6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompressionStage.next_action_mul line 80
  7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompressionStage.next_action_original line 93
  8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompressionStage.next_agreement line 98
  9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompressionStage.next_negative line 110
  10. def OAI.PartitionPilot.Compression.RecursiveMaps.CompressionStage.next line 122
  11. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.firstStage line 146
  12. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.stages line 164
  13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.stages_agreement line 168
  14. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.Point line 189
  15. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.order line 191
  16. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.origin line 193
  17. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.step line 195
  18. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.compression line 198
  19. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.stageAction line 201
  20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.origins_coherent line 205
  21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.maps_coherent line 208
  22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.actions_coherent line 212
  23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.stage_bottom line 217
  24. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.stageAction_one line 223
  25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.stageAction_mul line 229
  26. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.stageAction_original line 236
  27. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.stage_equivariant line 243
  28. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.stage_agreement line 250
  29. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.stage_base_agreement line 258
  30. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.maps_base line 269
  31. def OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.cap line 275
  32. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.caps_coherent line 278
  33. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.range_below_cap line 282
  34. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.cap_separation line 286
  35. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.original_below_cap line 312
  36. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.cap_strict line 328
  37. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.separator_not_below_cap line 338
  38. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TaskSystem.stage_fresh_accounting line 342