OAI/SetTheory/PartitionPrinciple/Geometry/ExternalOwnerCoordinateLaws.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalIdentityCopyGraph line 19
  2. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalSeedCarrier line 22
  3. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalSeedHeight line 25
  4. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalIdentityCopyGraph_eq_graph line 50
  5. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalSeedCarrier_iff line 59
  6. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalSeedHeights_spec line 77
  7. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalSeedHeight_entry line 97
  8. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalStarOwner line 119
  9. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarOwner_iff line 150
  10. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarOwner_ground_function line 164
  11. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarOwner_subset line 216
  12. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarOwner_value_iff line 222
  13. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarOwner_eq_graph line 231
  14. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarOwner_order_depth line 242
  15. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarOwner_root_iff line 271
  16. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarOwner_fresh_tile line 302
  17. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarOwner_seed_iff line 360
  18. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalSeedCarrier_lower line 365
  19. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalSeedCarrier_no_new_below line 372
  20. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarOwner_order line 377
  21. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalTileCoordinates_support line 432
  22. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalTileCoordinates_owner_total line 456
  23. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalTileCoordinates_raw_strict line 467
  24. def OAI.PartitionPilot.Forcing.GroundExternalLocalHeightData.externalHeightGraph line 500
  25. structure OAI.PartitionPilot.Forcing.GroundExternalHeightData line 513
  26. def OAI.PartitionPilot.Forcing.GroundExternalHeightData.height line 535