OAI/Combinatorics/HoneycombBridges/Concatenation.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Bridge concatenation and single-crossing cuts.

  1. def OAI.HoneycombActual.shiftVertex line 14
  2. def OAI.HoneycombActual.concatenateVertices line 17
  3. def OAI.HoneycombActual.BridgeFactorizationLaw line 22
  4. theorem OAI.HoneycombActual.shiftVertex_col line 28
  5. theorem OAI.HoneycombActual.shiftVertex_row line 30
  6. theorem OAI.HoneycombActual.shiftVertex_side line 32
  7. theorem OAI.HoneycombActual.shiftVertex_up line 34
  8. theorem OAI.HoneycombActual.shiftVertex_down line 36
  9. theorem OAI.HoneycombActual.shiftVertex_zero line 38
  10. theorem OAI.HoneycombActual.shiftVertex_shift line 40
  11. theorem OAI.HoneycombActual.shiftVertex_injective line 44
  12. theorem OAI.HoneycombActual.shiftVertex_adj line 49
  13. theorem OAI.HoneycombActual.Bridge.vertices_ne_nil line 60
  14. def OAI.HoneycombActual.Bridge.concat line 65
  15. theorem OAI.HoneycombActual.Bridge.concat_vertices line 107
  16. theorem OAI.HoneycombActual.Bridge.concat_height line 109
  17. theorem OAI.HoneycombActual.Bridge.concat_terminal line 110
  18. theorem OAI.HoneycombActual.Bridge.concat_length line 111
  19. theorem OAI.HoneycombActual.Bridge.concat_assoc line 114
  20. theorem OAI.HoneycombActual.weight_concat line 125
  21. def OAI.HoneycombActual.RenewalList.changes line 133
  22. theorem OAI.HoneycombActual.RenewalList.changes_nil line 136
  23. theorem OAI.HoneycombActual.RenewalList.changes_singleton line 137
  24. theorem OAI.HoneycombActual.RenewalList.changes_cons_cons line 140
  25. theorem OAI.HoneycombActual.RenewalList.constant_of_changes_zero line 145
  26. theorem OAI.HoneycombActual.RenewalList.split_of_changes_one line 158
  27. def OAI.HoneycombActual.below line 186
  28. theorem OAI.HoneycombActual.crosses_eq_change line 188
  29. theorem OAI.HoneycombActual.crossingCount_eq_changes line 193
  30. theorem OAI.HoneycombActual.upward_crossing_shape line 200
  31. theorem OAI.HoneycombActual.Bridge.split_at_of_crossingCount_one line 219
  32. theorem OAI.HoneycombActual.RenewalList.changes_zero_of_constant line 303
  33. theorem OAI.HoneycombActual.RenewalList.changes_append line 314
  34. theorem OAI.HoneycombActual.RenewalList.takeWhile_append_of_sides line 332
  35. theorem OAI.HoneycombActual.Bridge.concat_crossing_at line 350
  36. theorem OAI.HoneycombActual.Bridge.concat_crossing_below line 370
  37. theorem OAI.HoneycombActual.Bridge.takeWhile_concat line 389
  38. theorem OAI.HoneycombActual.Bridge.concat_first_eq_of_height_eq line 399
  39. theorem OAI.HoneycombActual.Bridge.concat_left_cancel line 407
  40. theorem OAI.HoneycombActual.Bridge.concat_irreducible_first_height_eq line 414