OAI/SetTheory/PartitionPrinciple/Geometry/GroundTileStarIncidence.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.tileStarVertexCarrier line 11
  2. def OAI.PartitionPilot.Forcing.tileStarEdgeCarrier line 12
  3. def OAI.PartitionPilot.Forcing.tileStarDartCarrier line 13
  4. def OAI.PartitionPilot.Forcing.signedPresentation line 15
  5. def OAI.PartitionPilot.Forcing.tileStarVertexPresentation line 36
  6. def OAI.PartitionPilot.Forcing.tileStarEdgePresentation line 37
  7. def OAI.PartitionPilot.Forcing.tileStarDartPresentation line 38
  8. theorem OAI.PartitionPilot.Forcing.tileStarPresentations_carriers line 40
  9. theorem OAI.PartitionPilot.Forcing.tileStarVertexPresentation_encode line 45
  10. theorem OAI.PartitionPilot.Forcing.tileStarDartPresentation_encode line 51
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.tileStarCarriers_mem line 61
  12. def OAI.PartitionPilot.Forcing.TileStarSourceEntry line 82
  13. def OAI.PartitionPilot.Forcing.TileStarReverseEntry line 93
  14. def OAI.PartitionPilot.Forcing.tileStarSourceGraph line 98
  15. def OAI.PartitionPilot.Forcing.tileStarReverseGraph line 103
  16. def OAI.PartitionPilot.Forcing.tileStarTargetGraph line 108
  17. def OAI.PartitionPilot.Forcing.dartIncidenceGraph line 112
  18. def OAI.PartitionPilot.Forcing.dartAdjacencyGraph line 113
  19. theorem OAI.PartitionPilot.Forcing.pair_mem_tileStarSourceGraph line 116
  20. theorem OAI.PartitionPilot.Forcing.pair_mem_tileStarReverseGraph line 128
  21. def OAI.PartitionPilot.Forcing.BoundedFormula.tileStarSourceFormula line 142
  22. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_tileStarSourceFormula line 145
  23. def OAI.PartitionPilot.Forcing.BoundedFormula.tileStarReverseFormula line 157
  24. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_tileStarReverseFormula line 160
  25. def OAI.PartitionPilot.Forcing.BoundedFormula.tileStarSourceEntryFormula line 168
  26. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_tileStarSourceEntryFormula line 172
  27. def OAI.PartitionPilot.Forcing.BoundedFormula.tileStarReverseEntryFormula line 189
  28. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_tileStarReverseEntryFormula line 193
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.tileStarSourceGraph_mem line 218
  30. theorem OAI.PartitionPilot.Forcing.TransitiveGround.tileStarReverseGraph_mem line 241
  31. theorem OAI.PartitionPilot.Forcing.TransitiveGround.tileStarTargetGraph_mem line 264
  32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.dartIncidenceGraph_mem line 275
  33. theorem OAI.PartitionPilot.Forcing.TransitiveGround.dartAdjacencyGraph_mem line 280