OAI/Combinatorics/HalvingLines/Labels.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PlanarHalving.RankCoordinates.Family line 11
  2. def OAI.PlanarHalving.RankCoordinates.Family.value line 18
  3. lemma OAI.PlanarHalving.RankCoordinates.Family.continuous_value line 22
  4. def OAI.PlanarHalving.RankCoordinates.Family.flat line 25
  5. def OAI.PlanarHalving.Batches.System.rankFamily line 38
  6. lemma OAI.PlanarHalving.Batches.System.rankFamily_spec line 48
  7. abbrev OAI.PlanarHalving.Batches.Labels line 59
  8. instance OAI.PlanarHalving.Batches.labelsMetric line 61
  9. def OAI.PlanarHalving.Batches.System.labels line 63
  10. lemma OAI.PlanarHalving.Batches.System.continuous_labels line 66
  11. lemma OAI.PlanarHalving.Batches.System.coordinate_oscillation line 70
  12. lemma OAI.PlanarHalving.CompactLabels.ediam_le_finite line 88
  13. lemma OAI.PlanarHalving.CompactLabels.finite_tail line 103
  14. lemma OAI.PlanarHalving.CompactLabels.long_count_bound line 109
  15. theorem OAI.PlanarHalving.Limits.finiteMeasure_subsequence_dependent line 138
  16. def OAI.PlanarHalving.TimeWindows.Before line 165
  17. lemma OAI.PlanarHalving.TimeWindows.stop_le_start line 168
  18. lemma OAI.PlanarHalving.Batches.System.timeWindow_disjoint line 177
  19. lemma OAI.PlanarHalving.Batches.System.timeWindow_graph_gap line 189
  20. def OAI.PlanarHalving.Batches.System.windowCrossings line 201
  21. lemma OAI.PlanarHalving.Batches.System.windowCrossings_sub line 208
  22. def OAI.PlanarHalving.Batches.System.windowCrossPoint line 211
  23. lemma OAI.PlanarHalving.Batches.System.windowCrossPoint_injective line 215
  24. lemma OAI.PlanarHalving.Batches.System.windowCrossPoint_exterior line 222
  25. lemma OAI.PlanarHalving.Batches.System.windowCrossPoint_graph line 243
  26. theorem OAI.PlanarHalving.Batches.System.window_crossing_slots line 258
  27. lemma OAI.PlanarHalving.Batches.System.vertexMeasure_mass_le line 294
  28. def OAI.PlanarHalving.Batches.System.windowCrossMeasure line 302
  29. lemma OAI.PlanarHalving.Batches.System.windowCrossMeasure_mass_le line 306
  30. structure OAI.PlanarHalving.RankLimits.Configuration line 330
  31. instance OAI.PlanarHalving.RankLimits.(instance at line 342) line 342
  32. instance OAI.PlanarHalving.RankLimits.(instance at line 343) line 343
  33. instance OAI.PlanarHalving.RankLimits.(instance at line 344) line 344
  34. def OAI.PlanarHalving.RankLimits.Configuration.label line 346
  35. lemma OAI.PlanarHalving.RankLimits.Configuration.continuous_label line 348
  36. def OAI.PlanarHalving.RankLimits.Configuration.points line 351
  37. def OAI.PlanarHalving.RankLimits.Configuration.vertices line 353
  38. def OAI.PlanarHalving.RankLimits.Configuration.edgeTime line 355
  39. def OAI.PlanarHalving.RankLimits.Configuration.crossings line 357
  40. def OAI.PlanarHalving.RankLimits.Configuration.timeRestrict line 359
  41. lemma OAI.PlanarHalving.RankLimits.Configuration.points_mass line 362
  42. lemma OAI.PlanarHalving.RankLimits.Configuration.vertices_mass_le line 365
  43. lemma OAI.PlanarHalving.RankLimits.Configuration.edgeTime_mass line 367
  44. lemma OAI.PlanarHalving.RankLimits.Configuration.crossings_mass_le line 368
  45. lemma OAI.PlanarHalving.RankLimits.Configuration.timeRestrict_mass_le line 370