OAI/Combinatorics/SumProduct/Alignment/WordPlan02.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ConstructedWordPlan.GlobalWordPlan.Slots line 22
  2. abbrev OAI.ConstructedWordPlan.GlobalWordPlan.Shifts line 23
  3. def OAI.ConstructedWordPlan.GlobalWordPlan.unitShift line 25
  4. def OAI.ConstructedWordPlan.GlobalWordPlan.generators line 27
  5. def OAI.ConstructedWordPlan.GlobalWordPlan.terminalShift line 30
  6. def OAI.ConstructedWordPlan.GlobalWordPlan.jumpSlot line 33
  7. lemma OAI.ConstructedWordPlan.GlobalWordPlan.lift_map line 36
  8. lemma OAI.ConstructedWordPlan.GlobalWordPlan.jump_map line 44
  9. lemma OAI.ConstructedWordPlan.GlobalWordPlan.jump_slot line 57
  10. abbrev OAI.ConstructedWordPlan.GlobalWordPlan.OwnSubset line 63
  11. abbrev OAI.ConstructedWordPlan.GlobalWordPlan.Comparison line 65
  12. def OAI.ConstructedWordPlan.GlobalWordPlan.palette line 74
  13. def OAI.ConstructedWordPlan.GlobalWordPlan.centerReading line 78
  14. def OAI.ConstructedWordPlan.GlobalWordPlan.translatedReading line 83
  15. lemma OAI.ConstructedWordPlan.GlobalWordPlan.own_state_reading line 91
  16. def OAI.ConstructedWordPlan.GlobalWordPlan.closedOption line 127
  17. lemma OAI.ConstructedWordPlan.GlobalWordPlan.closed_cover line 133
  18. lemma OAI.ConstructedWordPlan.GlobalWordPlan.centerReading_continuous line 176
  19. lemma OAI.ConstructedWordPlan.GlobalWordPlan.translatedReading_continuous line 183
  20. lemma OAI.ConstructedWordPlan.GlobalWordPlan.closedOption_isClosed line 193
  21. def OAI.RationalLattice.shearedPoint line 222
  22. lemma OAI.RationalLattice.weightedShear_imageLaw line 226
  23. theorem OAI.RationalLattice.weightedCover_finite_closed_mass line 245