OAI/Combinatorics/SumProduct/Alignment/PairTail03.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PairTail.pairLevel line 30
  2. def OAI.PairTail.reducedLevel line 33
  3. lemma OAI.PairTail.mem_pairLevel line 37
  4. theorem OAI.PairTail.reducedLevel_coordinates line 49
  5. def OAI.PairTail.levelIndices line 92
  6. def OAI.PairTail.levelEmbedding line 95
  7. lemma OAI.PairTail.mem_range_levelEmbedding line 99
  8. lemma OAI.PairTail.reducedLevel_subspace line 107
  9. def OAI.PairTail.reducedLevelCoordinates line 137
  10. lemma OAI.PairTail.reducedLevel_lattice line 144
  11. lemma OAI.RationalLattice.coordinates_connected line 165
  12. lemma OAI.RationalLattice.coordinates_simplyConnected line 169
  13. lemma OAI.RationalLattice.coordinates_locallyCompact line 173
  14. lemma OAI.RationalLattice.coordinates_secondCountable line 177
  15. lemma OAI.PairTail.reducedLevel_connected line 198
  16. lemma OAI.PairTail.reducedLevel_simplyConnected line 203
  17. lemma OAI.PairTail.reducedLevel_compact_reps line 211
  18. lemma OAI.PairTail.reducedLevel_discrete line 221
  19. lemma OAI.PairTail.reducedLevelHaar_existsUnique line 232