OAI/RingTheory/BassTrace/CellTriangulation.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BassTrace.Sparse.Cuts.activeConstraints line 20
  2. lemma OAI.BassTrace.Sparse.Cuts.mem_activeConstraints line 23
  3. lemma OAI.BassTrace.Sparse.Cuts.exists_extrapolate_mem line 28
  4. lemma OAI.BassTrace.Sparse.Cuts.activeConstraints_injOn_extremePoints line 55
  5. lemma OAI.BassTrace.Sparse.Cuts.finite_extremePoints_cell line 71
  6. def OAI.BassTrace.Sparse.Cuts.polyhedronVertices line 78
  7. lemma OAI.BassTrace.Sparse.Cuts.mem_polyhedronVertices line 81
  8. lemma OAI.BassTrace.Sparse.Cuts.exists_extreme_maximizer line 89
  9. lemma OAI.BassTrace.Sparse.Cuts.exists_vertex_maximizer line 97
  10. lemma OAI.BassTrace.Sparse.Cuts.cell_eq_convexHull_vertices line 103
  11. lemma OAI.BassTrace.Sparse.Cuts.isClosed_cell line 131
  12. lemma OAI.BassTrace.Sparse.Cuts.cell_eq_convexHull_of_bounded line 136
  13. def OAI.BassTrace.Sparse.Cuts.CellData.ofBounded line 141
  14. def OAI.BassTrace.Sparse.Cuts.signedForm line 151
  15. def OAI.BassTrace.Sparse.Cuts.signedBound line 154
  16. def OAI.BassTrace.Sparse.Cuts.cutCell line 157
  17. lemma OAI.BassTrace.Sparse.Cuts.cutCell_nonempty_data line 160
  18. lemma OAI.BassTrace.Sparse.Cuts.cutCell_inter_supporting line 183
  19. lemma OAI.BassTrace.Sparse.Cuts.cutCell_cover line 220
  20. lemma OAI.BassTrace.Sparse.Cuts.SupportingFace.inter_restrict line 246
  21. lemma OAI.BassTrace.Sparse.Cuts.cutCell_inter_parents_supporting line 254
  22. def OAI.BassTrace.Sparse.Cuts.cutParents line 266
  23. lemma OAI.BassTrace.Sparse.Cuts.mem_cutParents line 273
  24. theorem OAI.BassTrace.Sparse.Cuts.exists_cutTriangulation line 285
  25. lemma OAI.BassTrace.Sparse.Cuts.affine_decomp_apply line 344
  26. theorem OAI.BassTrace.Sparse.Cuts.simplex_has_cellData line 347
  27. lemma OAI.BassTrace.Sparse.Cuts.simplex_affine_indicator line 434
  28. lemma OAI.BassTrace.Sparse.Cuts.simplex_face_supporting line 455
  29. theorem OAI.BassTrace.Sparse.Cuts.exists_simplicialCutTriangulation line 487