OAI/Probability/LatticeSurface/Convexity/ProductGraph.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FeasibleShift.DisjointUnion.graph line 34
  2. lemma OAI.FeasibleShift.DisjointUnion.graph_adj_same line 41
  3. lemma OAI.FeasibleShift.DisjointUnion.graph_adj_index line 47
  4. def OAI.FeasibleShift.DisjointUnion.sites line 50
  5. lemma OAI.FeasibleShift.DisjointUnion.mem_sites line 54
  6. lemma OAI.FeasibleShift.DisjointUnion.sites_card line 58
  7. def OAI.FeasibleShift.DisjointUnion.inclusion line 61
  8. lemma OAI.FeasibleShift.DisjointUnion.reachable_index line 69
  9. lemma OAI.FeasibleShift.DisjointUnion.reachable_same line 78
  10. lemma OAI.FeasibleShift.DisjointUnion.component_same line 98
  11. def OAI.FeasibleShift.DisjointUnion.freeEquiv line 110
  12. def OAI.FeasibleShift.DisjointUnion.heightEquiv line 117
  13. lemma OAI.FeasibleShift.DisjointUnion.heightEquiv_apply line 123
  14. lemma OAI.FeasibleShift.DisjointUnion.extendHeight_same line 128
  15. lemma OAI.FeasibleShift.DisjointUnion.polytope_same line 136
  16. lemma OAI.FeasibleShift.DisjointUnion.contactGraph_same line 156
  17. lemma OAI.FeasibleShift.DisjointUnion.shiftGraph_same line 166
  18. lemma OAI.FeasibleShift.DisjointUnion.prescription_same line 175
  19. lemma OAI.FeasibleShift.DisjointUnion.averagedShift_same line 186
  20. lemma OAI.FeasibleShift.DisjointUnion.neighbors_same line 193
  21. lemma OAI.FeasibleShift.DisjointUnion.localSites_same line 207
  22. lemma OAI.FeasibleShift.DisjointUnion.freeShift_same line 221