OAI/Analysis/PlanarPacking/TailHead.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpPlanar.shortNode line 7
  2. lemma OAI.SharpPlanar.shortNode_inj line 8
  3. lemma OAI.SharpPlanar.shortNode_le line 9
  4. lemma OAI.SharpPlanar.shortNode_cover_check line 10
  5. lemma OAI.SharpPlanar.shortNode_range line 12
  6. abbrev OAI.SharpPlanar.HeadNodeIndex line 18
  7. def OAI.SharpPlanar.headNodeNat line 19
  8. def OAI.SharpPlanar.headC line 22
  9. def OAI.SharpPlanar.headD line 25
  10. def OAI.SharpPlanar.headRational line 28
  11. lemma OAI.SharpPlanar.headNodeNat_le line 30
  12. lemma OAI.SharpPlanar.headData_low line 34
  13. lemma OAI.SharpPlanar.head_series_finite line 37
  14. lemma OAI.SharpPlanar.head_rational_factor line 54