OAI/Combinatorics/SumProduct/Alignment/Blocks01.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SourceChartedMenu.Menu line 33
  2. abbrev OAI.SourceChartedMenu.Menu.productG line 48
  3. abbrev OAI.SourceChartedMenu.Menu.productΓ line 49
  4. def OAI.SourceChartedMenu.Menu.productChart line 51
  5. def OAI.SourceChartedMenu.Menu.productMetric line 54
  6. lemma OAI.SourceChartedMenu.Menu.productCompatible line 57
  7. structure OAI.SourceChartedMenu.Piece line 62
  8. def OAI.SourceChartedMenu.Piece.eval line 74
  9. def OAI.SourceChartedMenu.Piece.padG line 76
  10. def OAI.SourceChartedMenu.Piece.padX line 77
  11. def OAI.SourceChartedMenu.Piece.padObs line 78
  12. lemma OAI.SourceChartedMenu.Piece.pad_orbit line 81
  13. lemma OAI.SourceChartedMenu.Piece.pad_lip line 85
  14. lemma OAI.SourceChartedMenu.Piece.pad_range line 93
  15. lemma OAI.SourceChartedMenu.Piece.pad_bound line 96
  16. def OAI.SourceBlocks.Tail line 116
  17. instance OAI.SourceBlocks.blocks01TailFintype line 117
  18. def OAI.SourceBlocks.Added line 120
  19. lemma OAI.SourceBlocks.Added.lt line 124
  20. lemma OAI.SourceBlocks.Added.before line 133
  21. lemma OAI.SourceBlocks.Added.disjoint line 139
  22. def OAI.SourceBlocks.tailEnum line 148
  23. def OAI.SourceBlocks.PairIndex line 150
  24. instance OAI.SourceBlocks.blocks01PairIndexFintype line 152
  25. def OAI.SourceBlocks.pairEnum line 154
  26. def OAI.SourceBlocks.pivot line 157
  27. lemma OAI.SourceBlocks.pivot_index line 168
  28. lemma OAI.SourceBlocks.pivot_disjoint line 170
  29. def OAI.SourceBlocks.pivots line 175
  30. lemma OAI.SourceBlocks.pivots_ordered line 177
  31. lemma OAI.SourceBlocks.mem_pivots line 180
  32. abbrev OAI.SourceBlocks.Block line 184
  33. def OAI.SourceBlocks.Block.set line 186
  34. def OAI.SourceBlocks.Block.target line 188
  35. lemma OAI.SourceBlocks.block_target_tail line 190
  36. lemma OAI.SourceBlocks.block_target_set line 193
  37. lemma OAI.SourceBlocks.added_exists_iff line 199
  38. structure OAI.SourceChartedAlignment.Realizes line 232
  39. theorem OAI.SourceChartedAlignment.charted_step line 242
  40. theorem OAI.SourceChartedAlignment.local_of_charts line 267
  41. theorem OAI.SourceChartedAlignment.charted_alignment line 289