OAI/RingTheory/BassTrace/LocalCuts.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BassTrace.Sparse.Cuts.faceClosure_mono line 16
  2. lemma OAI.BassTrace.Sparse.Cuts.chainFaces_mono line 24
  3. lemma OAI.BassTrace.Sparse.Cuts.cutCell_extend_irrelevant line 29
  4. lemma OAI.BassTrace.Sparse.Cuts.cutParents_mono_irrelevant line 54
  5. lemma OAI.BassTrace.Sparse.Cuts.complexParents_mono line 65
  6. lemma OAI.BassTrace.Sparse.Cuts.finiteComplex_space_finiteHull line 72
  7. lemma OAI.BassTrace.Sparse.Cuts.finiteHull_of_respects line 88
  8. lemma OAI.BassTrace.Sparse.Cuts.cutParents_finiteHull_simplicial line 98
  9. lemma OAI.BassTrace.Sparse.Cuts.canonicalCenter_supporting_iff line 112
  10. lemma OAI.BassTrace.Sparse.Cuts.simplicialParents_inter_supporting line 127
  11. lemma OAI.BassTrace.Sparse.Cuts.cutParents_mono line 135
  12. lemma OAI.BassTrace.Sparse.Cuts.faceClosure_cutParents_filter line 142
  13. lemma OAI.BassTrace.Sparse.Cuts.canonical_chainFaces_restrict_parent line 175
  14. lemma OAI.BassTrace.Sparse.Cuts.cutCell_restrict_irrelevant line 195
  15. lemma OAI.BassTrace.Sparse.Cuts.cutParents_eq_irrelevant line 225
  16. lemma OAI.BassTrace.Sparse.Cuts.chainFaces_finite line 240
  17. structure OAI.BassTrace.Sparse.Cuts.LocalCutData line 246
  18. abbrev OAI.BassTrace.Sparse.Cuts.CutPatch line 254
  19. lemma OAI.BassTrace.Sparse.Cuts.finitePatch_le line 257
  20. def OAI.BassTrace.Sparse.Cuts.LocalCutData.patchIndices line 266
  21. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.patchIndices_mono line 268
  22. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.patch_vanish line 275
  23. def OAI.BassTrace.Sparse.Cuts.LocalCutData.patchTriangulation line 285
  24. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.patchTriangulation_faces line 292
  25. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.patchTriangulation_trace line 302
  26. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.patchTriangulation_mono line 311
  27. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.patchTriangulation_directed line 324
  28. def OAI.BassTrace.Sparse.Cuts.LocalCutData.globalComplex line 333
  29. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.globalComplex_space line 337
  30. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.globalComplex_carrier line 356
  31. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.globalComplex_trace line 363
  32. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.globalComplex_cut_trace line 378
  33. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.patchTriangulation_restrict_faces line 399
  34. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.globalComplex_restrict_faces line 428
  35. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.globalComplex_restrict_finite line 451
  36. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.globalComplex_restrict_space line 456
  37. lemma OAI.BassTrace.Sparse.Cuts.cutCell_reindex line 471
  38. lemma OAI.BassTrace.Sparse.Cuts.cutParents_reindex line 488