OAI/Geometry/TranslativeCovering/CellMatching.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CellMatching.IsMatching line 31
  2. abbrev OAI.CellMatching.Matching line 35
  3. abbrev OAI.CellMatching.Classes line 38
  4. def OAI.CellMatching.rightClass line 40
  5. lemma OAI.CellMatching.rightClass_of_edge line 44
  6. lemma OAI.CellMatching.rightClass_unmatched line 51
  7. lemma OAI.CellMatching.inl_eq_rightClass line 56
  8. lemma OAI.CellMatching.rightClass_injective line 67
  9. def OAI.CellMatching.exactMatching line 80
  10. lemma OAI.CellMatching.mem_exactMatching line 90
  11. abbrev OAI.CellMatching.ExactPair line 94
  12. def OAI.CellMatching.expand line 97
  13. def OAI.CellMatching.collapse line 103
  14. lemma OAI.CellMatching.collapse_right line 111
  15. def OAI.CellMatching.diagramEquiv line 118
  16. def OAI.CellMatching.classIncidence line 135
  17. lemma OAI.CellMatching.incidence_equiv line 140
  18. def OAI.CellMatching.support line 171
  19. def OAI.CellMatching.jointWeight line 173
  20. lemma OAI.CellMatching.expansion_support line 177
  21. lemma OAI.CellMatching.expansion_weight line 194
  22. def OAI.CellMatching.pairWeight line 199
  23. lemma OAI.CellMatching.diagram_sum line 203
  24. lemma OAI.CellMatching.support_inter_nonempty_iff line 216
  25. def OAI.CellMatching.allDiagramsEquiv line 240
  26. lemma OAI.CellMatching.all_diagram_sum line 254
  27. lemma OAI.CellMatching.matching_eq line 267
  28. lemma OAI.CellMatching.dependency_diagram_sum line 273