OAI/RingTheory/BassTrace/GraphRealization.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BassTrace.Sparse.GraphGeometry.graphMetric line 19
  2. lemma OAI.BassTrace.Sparse.GraphGeometry.graphMetric_discrete line 28
  3. def OAI.BassTrace.Sparse.GraphGeometry.neighborhood line 37
  4. lemma OAI.BassTrace.Sparse.GraphGeometry.walk_end_mem_neighborhood line 41
  5. lemma OAI.BassTrace.Sparse.GraphGeometry.dist_le_mem_neighborhood line 55
  6. lemma OAI.BassTrace.Sparse.GraphGeometry.connected_set_diameter line 62
  7. lemma OAI.BassTrace.Sparse.GraphGeometry.meeting_simplex_vertices line 75
  8. theorem OAI.BassTrace.Sparse.GraphGeometry.finitely_many_meeting_top_simplices line 97
  9. def OAI.BassTrace.Sparse.GraphGeometry.realization line 115
  10. lemma OAI.BassTrace.Sparse.GraphGeometry.locallyFinite_top_simplices line 118
  11. lemma OAI.BassTrace.Sparse.GraphGeometry.isClosed_realization line 137
  12. lemma OAI.BassTrace.Sparse.GraphGeometry.isCompact_realized_closedBall line 153
  13. def OAI.BassTrace.Sparse.simplexEquiv line 187
  14. def OAI.BassTrace.Sparse.simplexHomeomorph line 194
  15. lemma OAI.BassTrace.Sparse.continuousOn_coeff_simplex line 205
  16. lemma OAI.BassTrace.Sparse.GraphGeometry.finitely_many_top_simplices_at line 223
  17. lemma OAI.BassTrace.Sparse.GraphGeometry.continuousOn_coeff_realization line 234
  18. def OAI.BassTrace.Sparse.GraphGeometry.affineRealization line 249
  19. def OAI.BassTrace.Sparse.GraphGeometry.affineProbability line 252
  20. lemma OAI.BassTrace.Sparse.GraphGeometry.affineProbability_coeff line 262
  21. lemma OAI.BassTrace.Sparse.GraphGeometry.affineProbability_mem line 266
  22. lemma OAI.BassTrace.Sparse.GraphGeometry.locallyFinite_affine_top_simplices line 271
  23. lemma OAI.BassTrace.Sparse.GraphGeometry.continuous_affineProbability line 290
  24. def OAI.BassTrace.Sparse.GraphGeometry.realizationHomeomorph line 312