OAI/RingTheory/BassTrace/FaceFiltration.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BassTrace.Sparse.Cuts.vertexMean_weight_sum line 23
  2. lemma OAI.BassTrace.Sparse.Cuts.vertexMean_eq_sum line 27
  3. lemma OAI.BassTrace.Sparse.Cuts.vertexMean_mem_marked_iff line 31
  4. lemma OAI.BassTrace.Sparse.Cuts.segment_vertexMean_avoids line 44
  5. lemma OAI.BassTrace.Sparse.Cuts.vertexMean_components_eq line 87
  6. def OAI.BassTrace.Sparse.Cuts.PointFiltration.FinalFace line 114
  7. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.final_marked line 116
  8. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.final_mean_in_top line 119
  9. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.exists_face_level line 128
  10. def OAI.BassTrace.Sparse.Cuts.PointFiltration.faceLevel line 131
  11. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.faceLevel_le line 133
  12. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.mean_mem_faceLevel line 136
  13. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.mean_notMem_below_level line 139
  14. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.mean_mem_iff_level_le line 145
  15. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.hull_mem_iff_level_le line 151
  16. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.faceLevel_mono line 156
  17. def OAI.BassTrace.Sparse.Cuts.PointFiltration.below line 162
  18. def OAI.BassTrace.Sparse.Cuts.PointFiltration.stratum line 164
  19. def OAI.BassTrace.Sparse.Cuts.PointFiltration.faceComponent line 166
  20. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.mean_mem_stratum line 169
  21. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.mean_mem_component line 177
  22. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.faceComponent_subset line 180
  23. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.faceComponent_eq_of_level_eq line 183
  24. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.final_face_card_le_level line 201
  25. lemma OAI.BassTrace.Sparse.zero_support_top line 234
  26. lemma OAI.BassTrace.Sparse.zero_isDiscrete line 256
  27. lemma OAI.BassTrace.Sparse.zero_component_subsingleton line 293
  28. lemma OAI.BassTrace.Sparse.GraphGeometry.original_card_bound line 323
  29. lemma OAI.BassTrace.Sparse.GraphGeometry.faceComponent_mem_space line 329
  30. lemma OAI.BassTrace.Sparse.GraphGeometry.faceComponent_distance line 338
  31. def OAI.BassTrace.Sparse.GraphGeometry.labelWindow line 367
  32. lemma OAI.BassTrace.Sparse.GraphGeometry.component_support_subset line 371
  33. def OAI.BassTrace.Sparse.supportVertices line 403
  34. lemma OAI.BassTrace.Sparse.supportVertices_mono line 406
  35. lemma OAI.BassTrace.Sparse.componentSupport_subset line 426
  36. lemma OAI.BassTrace.Sparse.componentSupport_finite line 435
  37. lemma OAI.BassTrace.Sparse.componentSupport_nonempty line 448