OAI/Combinatorics/ThinTrees/Pencil/BlockAssembly.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Block assembly.

  1. abbrev OAI.CurrentKS.Realization.BlocksData line 14
  2. abbrev OAI.CurrentKS.Realization.blocksCode line 15
  3. def OAI.CurrentKS.Realization.stitchEntry line 16
  4. def OAI.CurrentKS.Realization.stitchData line 27
  5. abbrev OAI.CurrentKS.Realization.stitchCode line 31
  6. abbrev OAI.CurrentKS.Realization.stFirst line 32
  7. abbrev OAI.CurrentKS.Realization.stBlocks line 33
  8. abbrev OAI.CurrentKS.Realization.stI line 34
  9. abbrev OAI.CurrentKS.Realization.stJ line 35
  10. abbrev OAI.CurrentKS.Realization.stN line 36
  11. abbrev OAI.CurrentKS.Realization.stTail line 37
  12. abbrev OAI.CurrentKS.Realization.stMatrices line 38
  13. abbrev OAI.CurrentKS.Realization.stScalars line 39
  14. def OAI.CurrentKS.Realization.stK line 40
  15. instance OAI.CurrentKS.Realization.poly_stK line 41
  16. def OAI.CurrentKS.Realization.stCut line 42
  17. instance OAI.CurrentKS.Realization.poly_stCut line 43
  18. def OAI.CurrentKS.Realization.stitchedMatrixEntry line 45
  19. instance OAI.CurrentKS.Realization.poly_stitchedMatrixEntry line 48
  20. def OAI.CurrentKS.Realization.stitchProgramEntry line 54
  21. instance OAI.CurrentKS.Realization.poly_stitchProgramEntry line 60
  22. def OAI.CurrentKS.Realization.stitchProgram line 66
  23. instance OAI.CurrentKS.Realization.poly_stitchProgram line 73
  24. lemma OAI.CurrentKS.Realization.stitch_top line 78
  25. lemma OAI.CurrentKS.Realization.stitch_top_bottom line 94
  26. lemma OAI.CurrentKS.Realization.stitch_bottom_top line 101
  27. lemma OAI.CurrentKS.Realization.stitch_bottom line 109
  28. def OAI.CurrentKS.Realization.blockRowEquiv line 119
  29. lemma OAI.CurrentKS.Realization.blockRowEquiv_left line 123
  30. lemma OAI.CurrentKS.Realization.blockRowEquiv_right line 125
  31. lemma OAI.CurrentKS.Realization.stitch_data line 128