OAI/RingTheory/BassTrace/CutNaturality.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BassTrace.Sparse.Cuts.vertexMean_affine_map line 17
2. lemma OAI.BassTrace.Sparse.Cuts.canonicalVertices_affine_map line 26
3. lemma OAI.BassTrace.Sparse.Cuts.canonicalCenter_affine_map line 35
4. lemma OAI.BassTrace.Sparse.Cuts.SupportingFace.affine_image_injective line 44
5. lemma OAI.BassTrace.Sparse.Cuts.SupportingFace.affine_preimage line 75
6. lemma OAI.BassTrace.Sparse.Cuts.cellFaces_affine_map_injective line 91
7. lemma OAI.BassTrace.Sparse.Cuts.RespectsSet.affine_image line 115
8. def OAI.BassTrace.Sparse.Cuts.CellTriangulation.affineImage line 125
9. lemma OAI.BassTrace.Sparse.Cuts.faceClosure_affine_map_injective line 153
10. theorem OAI.BassTrace.Sparse.Cuts.exists_canonical_cutTriangulation line 171
11. lemma OAI.BassTrace.Sparse.Cuts.chainFaces_map_injective line 231
12. lemma OAI.BassTrace.Sparse.Cuts.cutCell_linear_image line 294
13. lemma OAI.BassTrace.Sparse.Cuts.cutParents_linear_image line 307
14. lemma OAI.BassTrace.Sparse.Cuts.canonical_chainFaces_map_injective line 325
15. lemma OAI.BassTrace.Sparse.Cuts.faceClosure_finiteHull line 347
16. theorem OAI.BassTrace.Sparse.Cuts.exists_embedded_canonical_cutTriangulation line 358