OAI/Combinatorics/HoneycombBridges/Geometry.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Geometry of concatenation and vertex-port conventions.

  1. def OAI.HoneycombActual.BridgeGeometryLaw line 14
  2. def OAI.HoneycombActual.shiftPoint line 26
  3. theorem OAI.HoneycombActual.shiftPoint_port line 28
  4. theorem OAI.HoneycombActual.position_shiftVertex line 32
  5. theorem OAI.HoneycombActual.shiftPoint_isometry line 37
  6. theorem OAI.HoneycombActual.port_eq_midpoint line 42
  7. theorem OAI.HoneycombActual.Bridge.height_le_endpointDistance line 49
  8. theorem OAI.HoneycombActual.Bridge.concat_trace_subset line 57
  9. theorem OAI.HoneycombActual.Bridge.concat_diameter_le line 72
  10. theorem OAI.HoneycombActual.Bridge.concat_cut_mem_convexHull line 91
  11. theorem OAI.HoneycombActual.Bridge.left_trace_subset_convexHull_concat line 105
  12. theorem OAI.HoneycombActual.Bridge.right_trace_subset_convexHull_concat line 116
  13. theorem OAI.HoneycombActual.Bridge.le_concat_diameter line 134
  14. theorem OAI.HoneycombActual.bridgeProduct_height_sum line 154
  15. theorem OAI.HoneycombActual.bridgeProduct_diameter line 171
  16. theorem OAI.HoneycombActual.bridgeGeometry line 195
  17. def OAI.HoneycombActual.Bridge.vertexEndpointDistance line 208
  18. def OAI.HoneycombActual.Bridge.vertexTrace line 211
  19. def OAI.HoneycombActual.Bridge.vertexDiameter line 213
  20. def OAI.HoneycombActual.BoundedVertexConventions line 217
  21. theorem OAI.HoneycombActual.rowSpacing_nonneg line 222
  22. theorem OAI.HoneycombActual.port_dist_up line 226
  23. theorem OAI.HoneycombActual.port_dist_down line 234
  24. theorem OAI.HoneycombActual.Bridge.endpointDistance_vertex_change line 244
  25. theorem OAI.HoneycombActual.Bridge.vertexTrace_finite line 255
  26. theorem OAI.HoneycombActual.Bridge.first_vertex_mem_vertexTrace line 258
  27. theorem OAI.HoneycombActual.Bridge.last_vertex_mem_vertexTrace line 262
  28. theorem OAI.HoneycombActual.Bridge.vertexEndpointDistance_le_vertexDiameter line 266
  29. theorem OAI.HoneycombActual.Bridge.vertexDiameter_le_diameter line 271
  30. theorem OAI.HoneycombActual.Bridge.trace_near_vertexTrace line 274
  31. theorem OAI.HoneycombActual.Bridge.diameter_le_vertexDiameter_add line 282
  32. theorem OAI.HoneycombActual.Bridge.diameter_vertex_change line 293
  33. theorem OAI.HoneycombActual.boundedVertexConventions line 300