OAI/SetTheory/PartitionPrinciple/Geometry/CompressionExternalTileOverlaps.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PartitionPilot.Forcing.GroundCompressionCompletion line 13
  2. theorem OAI.PartitionPilot.Forcing.GroundCompressionUnionData.fields_unique line 46
  3. theorem OAI.PartitionPilot.Forcing.GroundCompressionUnionData.unique line 54
  4. theorem OAI.PartitionPilot.Forcing.GroundCompressionAlgebra.unique line 67
  5. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.unique line 83
  6. theorem OAI.PartitionPilot.Forcing.externalRectangleParameters_exists line 101
  7. def OAI.PartitionPilot.Forcing.externalRectangleParameters line 110
  8. theorem OAI.PartitionPilot.Forcing.externalRectangleParameters_spec line 115
  9. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalMap line 127
  10. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalMap_entry line 130
  11. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalCap line 134
  12. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalCap_entry line 138
  13. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalCopy line 143
  14. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalCopy_entry line 150
  15. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalRectangle line 160
  16. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalRectangle_fields line 167
  17. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalRequest line 179
  18. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamily line 190
  19. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamily_child line 198
  20. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamilyLetterEquiv line 202
  21. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamilyLetterPresentation line 210
  22. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamilyLetterPresentation_carrier line 226
  23. def OAI.PartitionPilot.Forcing.externalCompressionField line 240
  24. theorem OAI.PartitionPilot.Forcing.compressionProjection_entry_iff line 243
  25. theorem OAI.PartitionPilot.Forcing.externalCompressionField_entry_iff line 255
  26. theorem OAI.PartitionPilot.Forcing.externalCompressionField_function line 269
  27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalCompressionField_mem line 277
  28. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalMaps line 297
  29. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalCaps line 300
  30. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.external_fields_ground line 303
  31. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.external_fields_entries line 318
  32. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.external_fields_range line 326
  33. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.completion_of_accounting line 354
  34. structure OAI.PartitionPilot.Forcing.GroundHeightedCompression line 399
  35. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamily_compression_letter line 420
  36. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamily_separation_letter line 424
  37. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamily_rectangle_letter line 428
  38. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamilyVertexCode line 432
  39. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamilyVertexCode_root line 440
  40. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamilyVertexCode_compression line 444
  41. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamilyVertexCode_separation line 447
  42. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamilyVertexCode_rectangle line 450
  43. structure OAI.PartitionPilot.Forcing.GroundProfiledCompression line 461
  44. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalMaps_compression_iff line 482
  45. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalMaps_tag line 489
  46. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalMap_external_bound line 495
  47. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalOverlapForward_compression line 498
  48. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalOverlapForward_separation line 510
  49. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalOverlapForward_rectangle line 523
  50. structure OAI.PartitionPilot.Forcing.GroundBornCompression line 563
  51. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamily_diagonal_iff line 591
  52. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamily_compression_overlap line 598
  53. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamily_separation_overlap line 610
  54. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamily_rectangle_first_overlap line 626
  55. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamily_rectangle_second_overlap line 649
  56. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamily_rectangle_children_overlap line 672