OAI/Geometry/UnitDistances/Extraction.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.OrganizedProfiles.jump line 13
  2. def OAI.PlanarUnitDistances.OrganizedProfiles.ratio line 14
  3. theorem OAI.PlanarUnitDistances.OrganizedProfiles.log_ratio line 16
  4. lemma OAI.PlanarUnitDistances.OrganizedProfiles.ratio_supported line 23
  5. lemma OAI.PlanarUnitDistances.OrganizedProfiles.log_residual line 29
  6. lemma OAI.PlanarUnitDistances.OrganizedProfiles.height_lower line 45
  7. theorem OAI.PlanarUnitDistances.OrganizedProfiles.selected line 61
  8. theorem OAI.PlanarUnitDistances.OrganizedProfiles.identity line 83
  9. def OAI.PlanarUnitDistances.OrganizedGraph.edge line 107
  10. def OAI.PlanarUnitDistances.OrganizedGraph.label line 108
  11. lemma OAI.PlanarUnitDistances.OrganizedGraph.label_eq line 111
  12. theorem OAI.PlanarUnitDistances.OrganizedGraph.properties line 114
  13. def OAI.PlanarUnitDistances.IncidenceSelected.kept line 164
  14. def OAI.PlanarUnitDistances.IncidenceSelected.edge line 166
  15. def OAI.PlanarUnitDistances.IncidenceSelected.label line 167
  16. def OAI.PlanarUnitDistances.IncidenceSelected.pairs line 168
  17. lemma OAI.PlanarUnitDistances.IncidenceSelected.properties line 170
  18. lemma OAI.PlanarUnitDistances.IncidenceSelected.no_popular line 188
  19. lemma OAI.PlanarUnitDistances.IncidenceSelected.count line 195
  20. theorem OAI.PlanarUnitDistances.IncidenceSelected.choose line 223
  21. def OAI.PlanarUnitDistances.ImageRelation.image line 252
  22. def OAI.PlanarUnitDistances.ImageRelation.equiv line 253
  23. lemma OAI.PlanarUnitDistances.ImageRelation.equiv_val line 258
  24. lemma OAI.PlanarUnitDistances.ImageRelation.inv_val line 259
  25. def OAI.PlanarUnitDistances.ImageRelation.edge line 262
  26. def OAI.PlanarUnitDistances.ImageRelation.label line 264
  27. lemma OAI.PlanarUnitDistances.ImageRelation.edge_iff line 266
  28. lemma OAI.PlanarUnitDistances.ImageRelation.label_eq line 271
  29. lemma OAI.PlanarUnitDistances.ImageRelation.card line 274
  30. def OAI.PlanarUnitDistances.IncidenceComplex.pull line 297
  31. lemma OAI.PlanarUnitDistances.IncidenceComplex.pull_coord line 299
  32. def OAI.PlanarUnitDistances.IncidenceComplex.edge line 302
  33. def OAI.PlanarUnitDistances.IncidenceComplex.label line 304
  34. lemma OAI.PlanarUnitDistances.IncidenceComplex.edge_iff line 306
  35. lemma OAI.PlanarUnitDistances.IncidenceComplex.label_eq line 308
  36. lemma OAI.PlanarUnitDistances.IncidenceComplex.card line 310
  37. lemma OAI.PlanarUnitDistances.IncidenceComplex.z_pull line 313
  38. lemma OAI.PlanarUnitDistances.IncidenceComplex.w_pull line 316
  39. lemma OAI.PlanarUnitDistances.IncidenceComplex.nonzero line 319
  40. lemma OAI.PlanarUnitDistances.IncidenceComplex.large line 323
  41. lemma OAI.PlanarUnitDistances.IncidenceComplex.distance line 328
  42. lemma OAI.PlanarUnitDistances.IncidenceComplex.rectangle line 335
  43. lemma OAI.PlanarUnitDistances.IncidenceComplex.no_circle line 344