OAI/RingTheory/BassTrace/Subdivisions.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BassTrace.Sparse.Cuts.Subdivision line 15
  2. lemma OAI.BassTrace.Sparse.Cuts.complex_respects_simplex line 24
  3. lemma OAI.BassTrace.Sparse.Cuts.complex_restrict_finite line 38
  4. def OAI.BassTrace.Sparse.Cuts.Subdivision.original line 52
  5. lemma OAI.BassTrace.Sparse.Cuts.Subdivision.marked line 59
  6. lemma OAI.BassTrace.Sparse.Cuts.UniversalCuts.localFaces_finite line 84
  7. lemma OAI.BassTrace.Sparse.Cuts.UniversalCuts.restrict_finite line 87
  8. def OAI.BassTrace.Sparse.Cuts.UniversalCuts.refine line 97
  9. lemma OAI.BassTrace.Sparse.Cuts.UniversalCuts.refine_preserves_marked line 108
  10. structure OAI.BassTrace.Sparse.Cuts.SubdivisionFamily line 114
  11. def OAI.BassTrace.Sparse.Cuts.UniversalCuts.refineFamily line 124
  12. lemma OAI.BassTrace.Sparse.Cuts.SubdivisionFamily.finite_faces_on line 151
  13. lemma OAI.BassTrace.Sparse.Cuts.SubdivisionFamily.countable_faces line 163
  14. lemma OAI.BassTrace.Sparse.Cuts.SubdivisionFamily.countable_vertices line 175
  15. lemma OAI.BassTrace.Sparse.Cuts.SubdivisionFamily.exists_generic_level line 184
  16. def OAI.BassTrace.Sparse.Cuts.Refines line 210
  17. lemma OAI.BassTrace.Sparse.Cuts.refines_self line 213
  18. lemma OAI.BassTrace.Sparse.Cuts.UniversalCuts.refine_refines line 216
  19. structure OAI.BassTrace.Sparse.Cuts.MarkedFamily line 220
  20. def OAI.BassTrace.Sparse.Cuts.ComponentDiameter line 227
  21. def OAI.BassTrace.Sparse.Cuts.DimensionDrop line 231
  22. structure OAI.BassTrace.Sparse.Cuts.AdmissibleStep line 236
  23. lemma OAI.BassTrace.Sparse.Cuts.DimensionDrop.avoids_vertices line 246
  24. lemma OAI.BassTrace.Sparse.Cuts.Subdivision.preserves_marked line 271
  25. lemma OAI.BassTrace.Sparse.Cuts.Subdivision.carrier_in line 274
  26. lemma OAI.BassTrace.Sparse.Cuts.Subdivision.preserves_respects line 287
  27. lemma OAI.BassTrace.Sparse.Cuts.Subdivision.finite_on_respected line 309
  28. def OAI.BassTrace.Sparse.Cuts.Subdivision.trans line 319
  29. lemma OAI.BassTrace.Sparse.Cuts.Refines.trans line 333
  30. lemma OAI.BassTrace.Sparse.Cuts.Refines.preserves_marked line 339