OAI/Geometry/HeilbronnTriangle/LiftCollisions.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem355.LiftCollisions.Column line 13
  2. def OAI.Problem355.LiftCollisions.InBox line 15
  3. def OAI.Problem355.LiftCollisions.natColumn line 18
  4. def OAI.Problem355.LiftCollisions.intColumn line 21
  5. lemma OAI.Problem355.LiftCollisions.nonneg_of_inBox line 24
  6. lemma OAI.Problem355.LiftCollisions.intColumn_natColumn line 28
  7. lemma OAI.Problem355.LiftCollisions.natColumn_mem_box line 33
  8. def OAI.Problem355.LiftCollisions.project line 39
  9. lemma OAI.Problem355.LiftCollisions.project_intColumn line 42
  10. lemma OAI.Problem355.LiftCollisions.project_natColumn line 46
  11. theorem OAI.Problem355.LiftCollisions.card_equal_projection_pairs_le line 50
  12. theorem OAI.Problem355.LiftCollisions.uniform_collision_fraction_le line 86
  13. def OAI.Problem355.LiftCollisions.samplingShift line 109
  14. def OAI.Problem355.LiftCollisions.lifts line 111
  15. lemma OAI.Problem355.LiftCollisions.lifts_inBox line 114
  16. lemma OAI.Problem355.LiftCollisions.card_lifts line 125
  17. theorem OAI.Problem355.LiftCollisions.crt_uniform_collision_fraction_le line 134