OAI/Combinatorics/SumProduct/Alignment/RationalLattice07.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalPolynomialMap.contDiff line 22
  2. lemma OAI.RationalPolynomialMap.bounded_lipschitz line 34
  3. lemma OAI.RationalLattice.polynomialMap_comp line 67
  4. lemma OAI.RationalLattice.polynomialMap_inv line 71
  5. lemma OAI.RationalLattice.correction_eq_of_lower_eq line 109
  6. lemma OAI.RationalLattice.mul_lower_congr line 126
  7. lemma OAI.RationalLattice.conj_lower_congr line 136
  8. lemma OAI.RationalLattice.conj_coord_difference line 141
  9. lemma OAI.RationalLattice.conj_mul_coord_difference line 149
  10. def OAI.RationalLattice.truncate line 159
  11. lemma OAI.RationalLattice.truncate_coord_self line 161
  12. lemma OAI.RationalLattice.truncate_coord_lower line 163
  13. lemma OAI.RationalLattice.conj_mul_truncated line 166
  14. lemma OAI.RationalLattice.polynomialMap_truncate line 182
  15. def OAI.PairTail.joinHomeomorph line 202
  16. def OAI.PairTail.baseSection line 226
  17. lemma OAI.PairTail.section_spec line 229
  18. lemma OAI.PairTail.section_continuous line 232
  19. def OAI.PairTail.chartHomeomorph line 238
  20. lemma OAI.PairTail.chart_base line 245
  21. lemma OAI.PairTail.chart_tail line 252
  22. lemma OAI.PairTail.chart_one line 260
  23. lemma OAI.PairTail.chart_rebuild_base line 267