OAI/Combinatorics/SumProduct/Alignment/RationalTail01.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalLattice.expProduct_rational line 24
  2. lemma OAI.RationalLattice.expCoordinates_rational line 31
  3. lemma OAI.IntegerHyperplane.exists_last_nonzero line 47
  4. def OAI.IntegerHyperplane.deletedCutoff line 62
  5. lemma OAI.IntegerHyperplane.succAbove_lt_cutoff line 64
  6. lemma OAI.IntegerHyperplane.lift_prefix_zero_iff line 77
  7. lemma OAI.RationalCharacterKernel.kernelCoordinates_adapted line 111
  8. theorem OAI.RationalCharacterKernel.exists_rational_kernel_chart line 122
  9. def OAI.RationalTailCoordinates.embed line 173
  10. def OAI.RationalTailCoordinates.lift line 174
  11. lemma OAI.RationalTailCoordinates.lift_embed line 176
  12. lemma OAI.RationalTailCoordinates.lift_prefix line 178
  13. lemma OAI.RationalTailCoordinates.lift_continuous line 180
  14. def OAI.RationalTailCoordinates.coordinates line 188
  15. lemma OAI.RationalTailCoordinates.coord_lift line 190
  16. def OAI.RationalTailCoordinates.rebuild line 200
  17. lemma OAI.RationalTailCoordinates.coordinates_rebuild line 205
  18. lemma OAI.RationalTailCoordinates.rebuild_coordinates line 208
  19. lemma OAI.RationalTailCoordinates.coordinates_continuous line 212
  20. lemma OAI.RationalTailCoordinates.rebuild_continuous line 216
  21. def OAI.RationalTailCoordinates.tailHomeomorph line 220
  22. def OAI.RationalTailCoordinates.lowerLift line 228
  23. lemma OAI.RationalTailCoordinates.exists_correction line 231
  24. def OAI.RationalTailCoordinates.correction line 254
  25. lemma OAI.RationalTailCoordinates.mul_coord line 257
  26. def OAI.RationalTailCoordinates.tailCoordinates line 287
  27. lemma OAI.RationalTailCoordinates.tailCoordinates_rational line 293
  28. lemma OAI.RationalTailCoordinates.tailCoordinates_lattice line 305
  29. lemma OAI.RationalTailCoordinates.tailCoordinates_adapted line 320