OAI/RingTheory/BassTrace/MarkedSubdivisions.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BassTrace.Sparse.Cuts.Subdivision.carrier_marked line 15
2. structure OAI.BassTrace.Sparse.Cuts.PointFiltration line 40
3. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.refines line 54
4. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.subset line 59
5. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.iterated_drop line 64
6. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.dimension_bound line 95
7. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.card_lower_of_mem_zero line 107
8. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.zero_carrier line 118
9. lemma OAI.BassTrace.Sparse.Cuts.IsMarked.contains_of_positive_barycenter line 149
10. lemma OAI.BassTrace.Sparse.Cuts.IsMarked.face_in_union line 156
11. lemma OAI.BassTrace.Sparse.Cuts.dimensionDrop_union_levels line 168
12. lemma OAI.BassTrace.Sparse.Cuts.DimensionDrop.refine line 179
13. lemma OAI.BassTrace.Sparse.Cuts.IsMarked.inter_iInter line 202
14. def OAI.BassTrace.Sparse.Cuts.UniversalCuts.closedPatch line 218
15. def OAI.BassTrace.Sparse.Cuts.UniversalCuts.outerPatch line 221
16. def OAI.BassTrace.Sparse.Cuts.UniversalCuts.spherePatch line 224
17. lemma OAI.BassTrace.Sparse.Cuts.UniversalCuts.closedPatch_marked line 227
18. lemma OAI.BassTrace.Sparse.Cuts.UniversalCuts.outerPatch_marked line 237
19. lemma OAI.BassTrace.Sparse.Cuts.UniversalCuts.spherePatch_marked line 250
20. lemma OAI.BassTrace.Sparse.Cuts.UniversalCuts.spherePatches_dimensionDrop line 264
21. lemma OAI.BassTrace.Sparse.Cuts.MarkedFamily.set_localConstancy line 296
22. def OAI.BassTrace.Sparse.Cuts.MarkedFamily.ofSets line 311
23. def OAI.BassTrace.Sparse.Cuts.MarkedFamily.refine line 339
24. def OAI.BassTrace.Sparse.Cuts.MarkedFamily.inter line 346
25. lemma OAI.BassTrace.Sparse.Cuts.MarkedFamily.locallyConstant_active_union line 360