OAI/Combinatorics/HalvingLines/RankCoordinates.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PlanarHalving.RankCoordinates.UnitOpen line 8
  2. structure OAI.PlanarHalving.RankCoordinates.Coordinate line 10
  3. def OAI.PlanarHalving.RankCoordinates.Coordinate.level line 22
  4. lemma OAI.PlanarHalving.RankCoordinates.Coordinate.value_level line 25
  5. lemma OAI.PlanarHalving.RankCoordinates.Coordinate.level_value line 28
  6. lemma OAI.PlanarHalving.RankCoordinates.Coordinate.lt_level_iff line 31
  7. lemma OAI.PlanarHalving.RankCoordinates.Coordinate.level_lt_iff line 35
  8. lemma OAI.PlanarHalving.RankCoordinates.Coordinate.le_level_iff line 39
  9. lemma OAI.PlanarHalving.RankCoordinates.Coordinate.level_le_iff line 43
  10. lemma OAI.PlanarHalving.RankCoordinates.Coordinate.continuous_level line 47
  11. lemma OAI.PlanarHalving.RankCoordinates.Coordinate.level_slope line 66
  12. lemma OAI.PlanarHalving.RankCoordinates.exists_zero_of_strongAnti line 80
  13. def OAI.PlanarHalving.RankCoordinates.levelDiff line 96
  14. lemma OAI.PlanarHalving.RankCoordinates.continuous_levelDiff line 99
  15. lemma OAI.PlanarHalving.RankCoordinates.levelDiff_decay line 104
  16. lemma OAI.PlanarHalving.RankCoordinates.levelDiff_strictAnti line 111
  17. lemma OAI.PlanarHalving.RankCoordinates.exists_intersection line 118
  18. def OAI.PlanarHalving.RankCoordinates.intersectionX line 124
  19. lemma OAI.PlanarHalving.RankCoordinates.levelDiff_intersectionX line 127
  20. lemma OAI.PlanarHalving.RankCoordinates.lt_intersectionX_iff line 131
  21. lemma OAI.PlanarHalving.RankCoordinates.intersectionX_lt_iff line 136
  22. lemma OAI.PlanarHalving.RankCoordinates.continuous_intersectionX line 141
  23. def OAI.PlanarHalving.RankCoordinates.pairHomeomorph line 154
  24. def OAI.PlanarHalving.RankCoordinates.smoothed line 183
  25. lemma OAI.PlanarHalving.RankCoordinates.continuous_smoothed line 186
  26. lemma OAI.PlanarHalving.RankCoordinates.smoothed_mem line 191
  27. lemma OAI.PlanarHalving.RankCoordinates.strict_vertical_smoothed line 204
  28. lemma OAI.PlanarHalving.RankCoordinates.onto_vertical_smoothed line 214
  29. def OAI.PlanarHalving.RankCoordinates.smoothedCoordinate line 246
  30. lemma OAI.PlanarHalving.RankCoordinates.Coordinate.strictMono_along_level line 277
  31. lemma OAI.PlanarHalving.RankCoordinates.Coordinate.strictAnti_along_level line 287
  32. lemma OAI.PlanarHalving.RankCoordinates.value_pair_inverse_fst line 299
  33. lemma OAI.PlanarHalving.RankCoordinates.value_pair_inverse_snd line 303
  34. lemma OAI.PlanarHalving.RankCoordinates.pair_inverse_snd_levelA line 307
  35. lemma OAI.PlanarHalving.RankCoordinates.pair_inverse_snd_levelB line 310
  36. lemma OAI.PlanarHalving.RankCoordinates.inverseX_mono_left line 317
  37. lemma OAI.PlanarHalving.RankCoordinates.inverseX_anti_right line 331
  38. def OAI.PlanarHalving.RankCoordinates.inCoordinates line 345
  39. lemma OAI.PlanarHalving.RankCoordinates.inCoordinates_eq_levelA line 349
  40. lemma OAI.PlanarHalving.RankCoordinates.inCoordinates_eq_levelB line 355
  41. lemma OAI.PlanarHalving.RankCoordinates.inCoordinates_monotone_left line 364
  42. lemma OAI.PlanarHalving.RankCoordinates.inCoordinates_antitone_left line 372
  43. lemma OAI.PlanarHalving.RankCoordinates.inCoordinates_antitone_right line 380
  44. lemma OAI.PlanarHalving.RankCoordinates.inCoordinates_monotone_right line 388