OAI/RingTheory/BassTrace/CanonicalCells.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BassTrace.Sparse.Cuts.canonicalVertices line 17
  2. def OAI.BassTrace.Sparse.Cuts.canonicalCenter line 20
  3. lemma OAI.BassTrace.Sparse.Cuts.coe_canonicalVertices line 22
  4. lemma OAI.BassTrace.Sparse.Cuts.finite_extremePoints_finiteHull line 26
  5. lemma OAI.BassTrace.Sparse.Cuts.finiteHull_eq_canonicalVertices line 30
  6. lemma OAI.BassTrace.Sparse.Cuts.canonicalCenter_mem_finiteHull line 40
  7. lemma OAI.BassTrace.Sparse.Cuts.canonicalCenter_supports_finiteHull line 49
  8. lemma OAI.BassTrace.Sparse.Cuts.affine_image_extremePoints line 63
  9. lemma OAI.BassTrace.Sparse.Cuts.canonicalVertices_map line 72
  10. lemma OAI.BassTrace.Sparse.Cuts.canonicalCenter_map line 81
  11. def OAI.BassTrace.Sparse.Cuts.CellData.canonical line 92
  12. lemma OAI.BassTrace.Sparse.Cuts.CellData.canonical_center line 105
  13. theorem OAI.BassTrace.Sparse.Cuts.exists_canonical_cellTriangulation line 108
  14. lemma OAI.BassTrace.Sparse.Cuts.chainFaces_affine_map line 117
  15. lemma OAI.BassTrace.Sparse.Cuts.chainFaces_restrict line 139
  16. lemma OAI.BassTrace.Sparse.Cuts.canonical_chainFaces_affine_map line 159
  17. def OAI.BassTrace.Sparse.Cuts.cellFaces line 178
  18. def OAI.BassTrace.Sparse.Cuts.faceClosure line 181
  19. lemma OAI.BassTrace.Sparse.Cuts.mem_cellFaces line 184
  20. lemma OAI.BassTrace.Sparse.Cuts.mem_faceClosure line 189
  21. lemma OAI.BassTrace.Sparse.Cuts.SupportingFace.affine_image line 199
  22. lemma OAI.BassTrace.Sparse.Cuts.cellFaces_affine_map line 218
  23. lemma OAI.BassTrace.Sparse.Cuts.faceClosure_affine_map line 238
  24. theorem OAI.BassTrace.Sparse.Cuts.faceClosure_isCellFamily line 248
  25. theorem OAI.BassTrace.Sparse.Cuts.exists_canonical_parentTriangulation line 276
  26. lemma OAI.BassTrace.Sparse.Cuts.affineIndependent_map_finset line 314
  27. def OAI.BassTrace.Sparse.Cuts.affineImageComplex line 323
  28. lemma OAI.BassTrace.Sparse.Cuts.affineImageComplex_finite line 359
  29. lemma OAI.BassTrace.Sparse.Cuts.affineImageComplex_space line 363
  30. lemma OAI.BassTrace.Sparse.Cuts.affine_image_extremePoints_injective line 382
  31. def OAI.BassTrace.Sparse.Cuts.affinePreimageComplex line 404
  32. lemma OAI.BassTrace.Sparse.Cuts.affinePreimageComplex_finite line 431
  33. lemma OAI.BassTrace.Sparse.Cuts.affineImage_preimage_complex line 436