OAI/Probability/LatticeSurface/Convexity/ProductData.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.FeasibleShift.DisjointUnion.heightEquiv_volume line 24
  2. lemma OAI.FeasibleShift.DisjointUnion.equiv_measure_preimage line 29
  3. def OAI.FeasibleShift.DisjointUnion.combinedPolytope line 36
  4. lemma OAI.FeasibleShift.DisjointUnion.combinedPolytope_eq line 41
  5. lemma OAI.FeasibleShift.DisjointUnion.combinedPolytope_measurable line 46
  6. lemma OAI.FeasibleShift.DisjointUnion.combinedPolytope_volume line 51
  7. lemma OAI.FeasibleShift.DisjointUnion.combinedPolytope_positive line 54
  8. lemma OAI.FeasibleShift.DisjointUnion.combinedPolytope_finite line 58
  9. lemma OAI.FeasibleShift.DisjointUnion.combined_law line 62
  10. lemma OAI.FeasibleShift.DisjointUnion.box_fiber_same line 74
  11. def OAI.FeasibleShift.DisjointUnion.fiber line 85
  12. lemma OAI.FeasibleShift.DisjointUnion.mem_fiber line 89
  13. lemma OAI.FeasibleShift.DisjointUnion.sites_fiber line 92
  14. lemma OAI.FeasibleShift.DisjointUnion.fiber_card line 97
  15. def OAI.FeasibleShift.DisjointUnion.combinedBad line 100
  16. lemma OAI.FeasibleShift.DisjointUnion.combined_sparse line 103
  17. def OAI.FeasibleShift.DisjointUnion.combine line 119
  18. lemma OAI.FeasibleShift.DisjointUnion.combine_law line 180
  19. lemma OAI.FeasibleShift.DisjointUnion.combine_map line 183