OAI/Geometry/UnitDistances/Main.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.IncidenceDiagonal.delta line 10
  2. lemma OAI.PlanarUnitDistances.IncidenceDiagonal.delta_pos line 11
  3. lemma OAI.PlanarUnitDistances.IncidenceDiagonal.delta_le line 12
  4. lemma OAI.PlanarUnitDistances.IncidenceDiagonal.delta_limit line 16
  5. structure OAI.PlanarUnitDistances.IncidenceDiagonal.Data line 20
  6. theorem OAI.PlanarUnitDistances.IncidenceDiagonal.exists_data line 31
  7. def OAI.PlanarUnitDistances.IncidenceDiagonal.Data.t line 49
  8. def OAI.PlanarUnitDistances.IncidenceDiagonal.Data.P line 50
  9. def OAI.PlanarUnitDistances.IncidenceDiagonal.Data.E line 51
  10. def OAI.PlanarUnitDistances.IncidenceDiagonal.Data.K line 52
  11. instance OAI.PlanarUnitDistances.IncidenceDiagonal.Data.(instance at line 53) line 53
  12. instance OAI.PlanarUnitDistances.IncidenceDiagonal.Data.(instance at line 54) line 54
  13. instance OAI.PlanarUnitDistances.IncidenceDiagonal.Data.(instance at line 55) line 55
  14. def OAI.PlanarUnitDistances.IncidenceDiagonal.Data.e line 56
  15. def OAI.PlanarUnitDistances.IncidenceDiagonal.Data.ell line 57
  16. lemma OAI.PlanarUnitDistances.IncidenceDiagonal.Data.t_limit line 58
  17. lemma OAI.PlanarUnitDistances.IncidenceDiagonal.Data.J_limit line 59
  18. lemma OAI.PlanarUnitDistances.IncidenceDiagonal.Data.card_power line 61
  19. lemma OAI.PlanarUnitDistances.IncidenceDiagonal.Data.edge_power line 65
  20. lemma OAI.PlanarUnitDistances.IncidenceDiagonal.Data.residual_small line 75
  21. lemma OAI.PlanarUnitDistances.IncidenceDiagonal.Data.hypotheses line 92
  22. theorem OAI.PlanarUnitDistances.IncidenceDiagonal.impossible line 116
  23. theorem OAI.PlanarUnitDistances.main line 129

    Distinct definitions of this name: ComparatorChallenges/PlanarUnitDistances.lean:19 (same statement text; different proof or body). Qualify references as OAI.PlanarUnitDistances.main@path.