OAI/SetTheory/PartitionPrinciple/Geometry/GroundExternalProfilePreservation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.MeetEmbeddingCode.restrictSource line 13
  2. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_bottom line 40
  3. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.canonical_iterate_bottom line 59
  4. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_bottom line 74
  5. theorem OAI.PartitionPilot.Forcing.GroundCompressionOrigin.union_bottom line 97
  6. theorem OAI.PartitionPilot.Forcing.GroundCompressionOrigin.initial_union_bottom line 113
  7. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalOriginalEmbedding line 137
  8. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalOriginalEmbedding_entry_iff line 141
  9. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOriginalEmbedding_mem line 164
  10. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOriginalEmbedding_code line 168
  11. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOriginalEmbedding_order_iff line 177
  12. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOriginalEmbedding_equivariant line 186
  13. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOriginalEmbedding_agreement line 199
  14. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOriginalEmbedding_bottom line 233
  15. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.exists_externalOriginal_bottom line 245
  16. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOriginal_image_mem line 272
  17. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOriginal_top_strict line 280
  18. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOriginal_top_not_image line 288
  19. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalOriginal_filterImage_eq line 303
  20. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalBounded_original_capProfile line 334