OAI/SetTheory/PartitionPrinciple/Geometry/GroundMainTaskCapFulfillment.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.boundedCapImages line 18
  2. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.boundedCapImages_ground line 41
  3. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.boundedCapImages_function line 48
  4. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.boundedCapImages_entry_iff line 54
  5. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.bounded_compression_generator_agreement line 98
  6. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.bounded_compression_generator_top_iff line 135
  7. def OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.compressionCapImages line 172
  8. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.compressionCapImages_ground line 182
  9. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.compressionCapImages_function line 187
  10. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.compressionCapImages_profile line 194
  11. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.compressionCapImages_common_target_meet line 238
  12. def OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.insertionCapImages line 286
  13. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.insertionCapImages_ground line 296
  14. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.insertionCapImages_entry_iff line 305
  15. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.insertionCapImages_function line 321
  16. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.insertionCapImages_profile line 333
  17. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.insertionCapImages_meet line 351
  18. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.insertionCapImages_injection line 374
  19. def OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.taskCapValues line 405
  20. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.taskCapValues_ground line 421
  21. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.taskCapFamily line 432
  22. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.realize_taskCapFamily line 446