OAI/RingTheory/BassTrace/SupportGeometry.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BassTrace.Sparse.marked_localConstancy_window line 26
  2. lemma OAI.BassTrace.Sparse.connectedComponentIn_inter_of_subset line 54
  3. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.faceLevel_eq_of_window line 76
  4. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.stratum_inter_eq_of_window line 91
  5. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.faceComponent_eq_of_window line 103
  6. lemma OAI.BassTrace.Sparse.GraphGeometry.component_subset_window line 143
  7. lemma OAI.BassTrace.Sparse.GraphGeometry.faceComponents_eq_local line 156
  8. def OAI.BassTrace.Sparse.OrbitForms.componentVectorEmbedding line 195
  9. lemma OAI.BassTrace.Sparse.OrbitForms.componentVectorEmbedding_apply line 198
  10. lemma OAI.BassTrace.Sparse.OrbitForms.push_norm line 204
  11. def OAI.BassTrace.Sparse.OrbitForms.pushIsometry line 212
  12. def OAI.BassTrace.Sparse.OrbitForms.pushHomeomorph line 216
  13. def OAI.BassTrace.Sparse.OrbitForms.SeparatingFiltration.translateFace line 229
  14. lemma OAI.BassTrace.Sparse.OrbitForms.SeparatingFiltration.translateFace_mean line 233
  15. lemma OAI.BassTrace.Sparse.OrbitForms.SeparatingFiltration.push_mem_marked_iff line 238
  16. lemma OAI.BassTrace.Sparse.OrbitForms.SeparatingFiltration.translateFace_level line 247
  17. lemma OAI.BassTrace.Sparse.OrbitForms.SeparatingFiltration.push_mem_stratum_iff line 257
  18. lemma OAI.BassTrace.Sparse.OrbitForms.SeparatingFiltration.stratum_image line 263
  19. lemma OAI.BassTrace.Sparse.OrbitForms.SeparatingFiltration.translateFace_component line 275