OAI/Analysis/PlanarPacking/NodeIntervals.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpPlanar.Numerical.qSmall line 10
  2. def OAI.SharpPlanar.Numerical.qLarge line 12
  3. def OAI.SharpPlanar.Numerical.qBase line 14
  4. def OAI.SharpPlanar.Numerical.dSmall line 16
  5. def OAI.SharpPlanar.Numerical.dOther line 17
  6. def OAI.SharpPlanar.Numerical.dBase line 18
  7. lemma OAI.SharpPlanar.Numerical.qSmall_contains line 20
  8. lemma OAI.SharpPlanar.Numerical.qLarge_contains line 25
  9. lemma OAI.SharpPlanar.Numerical.qBase_contains line 30
  10. lemma OAI.SharpPlanar.Numerical.dSmall_contains line 32
  11. lemma OAI.SharpPlanar.Numerical.dOther_contains line 36
  12. lemma OAI.SharpPlanar.Numerical.dBase_contains line 40
  13. def OAI.SharpPlanar.Numerical.qBox line 43
  14. def OAI.SharpPlanar.Numerical.dBox line 44
  15. lemma OAI.SharpPlanar.Numerical.qBox_contains line 52
  16. lemma OAI.SharpPlanar.Numerical.dBox_contains line 64
  17. def OAI.SharpPlanar.Numerical.invBox line 76
  18. def OAI.SharpPlanar.Numerical.qiBox line 77
  19. lemma OAI.SharpPlanar.Numerical.qiBox_contains line 78
  20. def OAI.SharpPlanar.Numerical.inflate line 83
  21. lemma OAI.SharpPlanar.Numerical.inflate_contains line 84
  22. lemma OAI.SharpPlanar.Numerical.K_column_contains line 93
  23. lemma OAI.SharpPlanar.Numerical.S_column_value_contains line 99
  24. lemma OAI.SharpPlanar.Numerical.S_column_derivative_contains line 104