OAI/Combinatorics/IndependentSets/Geometry/GeometryNaming.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LargeIndependentSets.ShortestPaths.pathDistance_surjective line 12
  2. theorem OAI.LargeIndependentSets.ShortestPaths.cover_allPairs_exact line 27
  3. def OAI.LargeIndependentSets.GeometryNames.mixed line 50
  4. lemma OAI.LargeIndependentSets.GeometryNames.mixed_val line 55
  5. lemma OAI.LargeIndependentSets.GeometryNames.mixed_surjective line 59
  6. abbrev OAI.LargeIndependentSets.GeometryNames.StaticPoint line 74
  7. def OAI.LargeIndependentSets.GeometryNames.decode line 77
  8. lemma OAI.LargeIndependentSets.GeometryNames.decode_surjective line 82
  9. abbrev OAI.LargeIndependentSets.GeometryNames.Node line 91
  10. def OAI.LargeIndependentSets.GeometryNames.nodeDecode line 94
  11. lemma OAI.LargeIndependentSets.GeometryNames.nodeDecode_surjective line 97
  12. def OAI.LargeIndependentSets.GeometryNames.nodeEquiv line 105
  13. def OAI.LargeIndependentSets.GeometryNames.names line 110
  14. lemma OAI.LargeIndependentSets.GeometryNames.names_surjective line 113
  15. def OAI.LargeIndependentSets.GeometryNames.PointStep line 121
  16. def OAI.LargeIndependentSets.GeometryNames.QuestionStep line 126
  17. lemma OAI.LargeIndependentSets.GeometryNames.questionStep_iff line 131
  18. lemma OAI.LargeIndependentSets.GeometryNames.forward_iff line 152