OAI/SetTheory/PartitionPrinciple/Geometry/GroundProfiledExternalRequests.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.separation_generator_fixes line 43
  2. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.separation_generator_meet line 60
  3. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.compression_generator_restriction line 77
  4. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.compression_generator_top line 94
  5. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.compression_generator_agreement line 105
  6. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.rectangle_generators_roots line 152
  7. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.rectangle_generators_agree line 173
  8. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.rectangle_generators_root_meets line 190
  9. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.rectangle_generators_meet line 214
  10. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.external_identity_copy_value line 279
  11. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.external_identity_capProfile line 298
  12. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.external_identity_filter_ground line 310
  13. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.external_compression_generator_profile line 317
  14. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.rectangle_generators_full_ideals line 366
  15. theorem OAI.PartitionPilot.Forcing.GroundProfiledCompression.external_generator_profile line 455