OAI/RingTheory/BassTrace/BallComparison.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BassTrace.Sparse.OrbitForms.SeparatingFiltration.admissibleStep line 22
  2. lemma OAI.BassTrace.Sparse.GraphGeometry.measurable_realization line 53
  3. lemma OAI.BassTrace.Sparse.GraphGeometry.measurable_centerDistance line 77
  4. def OAI.BassTrace.Sparse.GraphGeometry.ballWindow line 92
  5. lemma OAI.BassTrace.Sparse.GraphGeometry.measurable_ballWindow line 97
  6. lemma OAI.BassTrace.Sparse.GraphGeometry.ballWindow_push line 121
  7. lemma OAI.BassTrace.Sparse.GraphGeometry.original_marked_subset_space line 138
  8. lemma OAI.BassTrace.Sparse.GraphGeometry.localOriginalArea_ballWindow line 146
  9. lemma OAI.BassTrace.Sparse.GraphGeometry.replacement_ballWindow line 163
  10. theorem OAI.BassTrace.Sparse.GraphGeometry.ae_exists_ball_step line 222
  11. lemma OAI.BassTrace.Sparse.activeWindow_mono line 266
  12. theorem OAI.BassTrace.Sparse.GraphGeometry.ae_open_ball_comparison line 315
  13. lemma OAI.BassTrace.Sparse.GraphGeometry.ae_local_ball_closed_eq_open line 384
  14. def OAI.BassTrace.Sparse.GraphGeometry.ballMass line 419
  15. lemma OAI.BassTrace.Sparse.GraphGeometry.ballMass_mono line 426