OAI/SetTheory/PartitionPrinciple/Geometry/GroundExternalLocalHeightFamilies.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTileVertexImages_entry_iff line 32
  2. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTileCarrier_image line 73
  3. def OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTilePresentation line 113
  4. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTilePresentation_carrier line 123
  5. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTileOrder_iff line 158
  6. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTileMeet_iff line 176
  7. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTileOrder_shape line 199
  8. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTileMeet_eq_canonical line 208
  9. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTileMeet_code line 232
  10. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTileVertexGraph_iff line 272
  11. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTileVertexGraph_eq line 291
  12. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTileVertexCode_mem line 319
  13. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTileVertexGraph_mem line 324
  14. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTileVertexGraph_family line 334
  15. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTileVertexGraph_code line 342
  16. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.exists_localTileHeight line 386
  17. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.exists_localHeightFamily line 435