OAI/Combinatorics/SumProduct/Alignment/TailCharacter01.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TailRefinementCharts.prefixVector line 29
  2. def OAI.TailRefinementCharts.prefixElement line 32
  3. def OAI.TailRefinementCharts.tail line 33
  4. lemma OAI.TailRefinementCharts.prefix_coord line 36
  5. lemma OAI.TailRefinementCharts.tail_coord line 40
  6. lemma OAI.TailRefinementCharts.prefix_product line 46
  7. lemma OAI.TailRefinementCharts.decompose line 65
  8. lemma OAI.TailRefinementCharts.prefix_congr line 80
  9. lemma OAI.TailRefinementCharts.prefix_mul_congr line 91
  10. theorem OAI.TailRefinementCharts.tail_character_mul line 105
  11. def OAI.BlockSplitCoordinates.blockMap line 145
  12. lemma OAI.BlockSplitCoordinates.blockMap_prefix line 149
  13. lemma OAI.BlockSplitCoordinates.blockMap_embed line 152
  14. lemma OAI.BlockSplitCoordinates.blockMap_comp line 157
  15. lemma OAI.BlockSplitCoordinates.blockMap_id line 167
  16. lemma OAI.BlockSplitCoordinates.blockMap_continuous line 177
  17. def OAI.BlockSplitCoordinates.blockHomeomorph line 186
  18. lemma OAI.BlockSplitCoordinates.blockMap_polynomial line 203
  19. lemma OAI.BlockSplitCoordinates.splitCoordinates_polynomial line 211
  20. def OAI.TailCharacterRechart.chartHomeomorph line 234
  21. lemma OAI.TailCharacterRechart.chart_prefix line 238
  22. lemma OAI.TailCharacterRechart.chart_head line 241
  23. lemma OAI.TailCharacterRechart.chart_tail line 247
  24. lemma OAI.TailCharacterRechart.chart_polynomial line 254
  25. lemma OAI.TailCharacterRechart.inverse_polynomial line 260
  26. lemma OAI.TailCharacterRechart.chart_one line 267
  27. lemma OAI.TailCharacterRechart.old_lower_congr line 281
  28. def OAI.TailCharacterRechart.lowerElement line 306
  29. lemma OAI.TailCharacterRechart.lowerElement_coord line 311
  30. lemma OAI.TailCharacterRechart.lowerElement_below line 317
  31. lemma OAI.TailCharacterRechart.lowerElement_at line 321
  32. lemma OAI.TailCharacterRechart.exists_correction line 326
  33. def OAI.TailCharacterRechart.correction line 347
  34. lemma OAI.TailCharacterRechart.correction_eval line 351
  35. lemma OAI.TailCharacterRechart.prefix_defect line 360
  36. lemma OAI.TailCharacterRechart.tail_defect line 378
  37. lemma OAI.TailCharacterRechart.chart_head_character line 405
  38. lemma OAI.TailCharacterRechart.head_mul line 413
  39. lemma OAI.TailCharacterRechart.prefix_lower_head line 421
  40. lemma OAI.TailCharacterRechart.head_defect line 429
  41. lemma OAI.TailCharacterRechart.mul_coord line 440
  42. def OAI.TailCharacterRechart.tailCharacterCoordinates line 459