OAI/RingTheory/BassTrace/ActivatedUnions.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BassTrace.Sparse.Cuts.activatedUnion line 18
2. def OAI.BassTrace.Sparse.Cuts.replacementSet line 21
3. lemma OAI.BassTrace.Sparse.Cuts.activatedUnion_marked line 25
4. lemma OAI.BassTrace.Sparse.Cuts.difference_activatedUnion_marked line 36
5. lemma OAI.BassTrace.Sparse.Cuts.replacementSet_marked line 67
6. lemma OAI.BassTrace.Sparse.Cuts.replacementSet_subset line 76
7. def OAI.BassTrace.Sparse.Cuts.MarkedFamily.replacement line 84
8. lemma OAI.BassTrace.Sparse.Cuts.sphereUnion_componentDiameter line 122
9. def OAI.BassTrace.Sparse.Cuts.UniversalCuts.sphereStep line 143