OAI/RingTheory/BassTrace/FiniteCells.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BassTrace.Sparse.Cuts.restrictComplex line 14
  2. lemma OAI.BassTrace.Sparse.Cuts.restrictComplex_le line 25
  3. lemma OAI.BassTrace.Sparse.Cuts.restrictComplex_finite line 28
  4. lemma OAI.BassTrace.Sparse.Cuts.mem_restrict_supporting line 32
  5. lemma OAI.BassTrace.Sparse.Cuts.restrictComplex_space_supporting line 54
  6. def OAI.BassTrace.Sparse.Cuts.glueComplex line 68
  7. lemma OAI.BassTrace.Sparse.Cuts.glueComplex_finite line 90
  8. lemma OAI.BassTrace.Sparse.Cuts.glueComplex_space line 97
  9. lemma OAI.BassTrace.Sparse.Cuts.cross_inter_of_supporting_agreement line 107
  10. def OAI.BassTrace.Sparse.Cuts.RespectsSet line 129
  11. lemma OAI.BassTrace.Sparse.Cuts.restrictComplex_space_of_respects line 132
  12. lemma OAI.BassTrace.Sparse.Cuts.hull_inter_of_supporting_eq line 159
  13. lemma OAI.BassTrace.Sparse.Cuts.respectsSet_of_supporting_eq line 180
  14. lemma OAI.BassTrace.Sparse.Cuts.cross_inter_of_respects line 188
  15. lemma OAI.BassTrace.Sparse.Cuts.mem_radialBoundary_of_supporting line 216
  16. def OAI.BassTrace.Sparse.Cuts.SupportingFace line 234
  17. lemma OAI.BassTrace.Sparse.Cuts.SupportingFace.subset line 238
  18. lemma OAI.BassTrace.Sparse.Cuts.supportingFace_self line 242
  19. lemma OAI.BassTrace.Sparse.Cuts.linear_le_on_convexHull line 246
  20. lemma OAI.BassTrace.Sparse.Cuts.SupportingFace.trans_finite_hull line 257
  21. lemma OAI.BassTrace.Sparse.Cuts.SupportingFace.restrict line 311
  22. lemma OAI.BassTrace.Sparse.Cuts.SupportingFace.supporting_inter line 319
  23. lemma OAI.BassTrace.Sparse.Cuts.SupportingFace.eq_convexHull_subset line 334
  24. lemma OAI.BassTrace.Sparse.Cuts.finite_supportingFaces line 345
  25. lemma OAI.BassTrace.Sparse.Cuts.SupportingFace.inter_of_parent_inter line 354
  26. structure OAI.BassTrace.Sparse.Cuts.CellData line 374
  27. lemma OAI.BassTrace.Sparse.Cuts.cell_reindex line 385
  28. def OAI.BassTrace.Sparse.Cuts.CellData.ofPresentation line 394
  29. lemma OAI.BassTrace.Sparse.Cuts.vertexMean_supports line 408
  30. def OAI.BassTrace.Sparse.Cuts.CellData.supportingFace line 418
  31. lemma OAI.BassTrace.Sparse.Cuts.CellData.center_notMem_proper_face line 452
  32. lemma OAI.BassTrace.Sparse.Cuts.CellData.face_subset_boundary line 459
  33. lemma OAI.BassTrace.Sparse.Cuts.CellData.boundary_mem_face line 475
  34. structure OAI.BassTrace.Sparse.Cuts.FiniteCellFamily line 486
  35. lemma OAI.BassTrace.Sparse.Cuts.FiniteCellFamily.erase_maximal line 491
  36. def OAI.BassTrace.Sparse.Cuts.familySpace line 506
  37. structure OAI.BassTrace.Sparse.Cuts.CellTriangulation line 508
  38. lemma OAI.BassTrace.Sparse.Cuts.CellTriangulation.respects_of_carrier line 515
  39. def OAI.BassTrace.Sparse.Cuts.CellTriangulation.extend line 523
  40. lemma OAI.BassTrace.Sparse.Cuts.CellTriangulation.mem_extend_faces line 590
  41. lemma OAI.BassTrace.Sparse.Cuts.CellData.center_mem_iff_subset line 610
  42. def OAI.BassTrace.Sparse.Cuts.chainFaces line 621
  43. lemma OAI.BassTrace.Sparse.Cuts.mem_chainFaces_erase_subset line 626
  44. lemma OAI.BassTrace.Sparse.Cuts.chainFaces_maximal line 634
  45. theorem OAI.BassTrace.Sparse.Cuts.exists_cellTriangulation line 693
  46. theorem OAI.BassTrace.Sparse.Cuts.exists_cellTriangulation_chains line 712
  47. theorem OAI.BassTrace.Sparse.Cuts.exists_cellTriangulation_parents line 748