OAI/RingTheory/BassTrace/BallReplacement.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BassTrace.Sparse.GraphGeometry.meeting_simplex_patch line 35
2. lemma OAI.BassTrace.Sparse.GraphGeometry.ballComplement_marked line 84
3. lemma OAI.BassTrace.Sparse.finite_translated_support_meeting line 137
4. lemma OAI.BassTrace.Sparse.GraphGeometry.finite_ball_incidence line 178
5. lemma OAI.BassTrace.Sparse.Cuts.SubdivisionFamily.countable_exceptional_levels line 221
6. theorem OAI.BassTrace.Sparse.GraphGeometry.exists_ball_replacement line 264