OAI/RingTheory/BassTrace/GeometricSubcomplexes.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Local finiteness passes to a simplexwise finite subdivision.

  1. lemma OAI.BassTrace.Sparse.locallyFinite_refinement line 17
  2. lemma OAI.BassTrace.Sparse.simplicial_refinement_locallyFinite line 31
  3. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.globalComplex_locallyFinite line 62
  4. def OAI.BassTrace.Sparse.Cuts.geometricRestriction line 82
  5. def OAI.BassTrace.Sparse.Cuts.IsMarked line 93
  6. lemma OAI.BassTrace.Sparse.Cuts.geometricRestriction_le line 97
  7. lemma OAI.BassTrace.Sparse.Cuts.IsMarked.subset_space line 100
  8. lemma OAI.BassTrace.Sparse.Cuts.IsMarked.restriction_space line 106
  9. lemma OAI.BassTrace.Sparse.Cuts.isMarked_empty line 117
  10. lemma OAI.BassTrace.Sparse.Cuts.isMarked_space line 121
  11. lemma OAI.BassTrace.Sparse.Cuts.isMarked_simplex line 126
  12. lemma OAI.BassTrace.Sparse.Cuts.IsMarked.sUnion line 130
  13. lemma OAI.BassTrace.Sparse.Cuts.IsMarked.iUnion line 137
  14. lemma OAI.BassTrace.Sparse.Cuts.IsMarked.union line 144
  15. lemma OAI.BassTrace.Sparse.Cuts.IsMarked.inter line 153
  16. lemma OAI.BassTrace.Sparse.Cuts.IsMarked.refinement line 168
  17. lemma OAI.BassTrace.Sparse.Cuts.card_lt_of_generic_hyperplane line 177
  18. lemma OAI.BassTrace.Sparse.Cuts.exists_branch_eq_on_simplex line 195
  19. lemma OAI.BassTrace.Sparse.Cuts.card_lt_of_generic_max_level line 205
  20. lemma OAI.BassTrace.Sparse.Cuts.exists_generic_level line 222
  21. lemma OAI.BassTrace.Sparse.Cuts.RespectsSet.isMarked line 246
  22. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.globalComplex_isMarked_simplex line 260
  23. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.globalComplex_preserves_marked line 267
  24. lemma OAI.BassTrace.Sparse.Cuts.cutParents_singleton_finiteHull line 283
  25. lemma OAI.BassTrace.Sparse.Cuts.canonicalCuts_linear_map line 302
  26. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.globalComplex_map line 338
  27. lemma OAI.BassTrace.Sparse.Cuts.exists_smallest_carrier line 365
  28. lemma OAI.BassTrace.Sparse.Cuts.IsMarked.iInter_space line 389
  29. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.globalComplex_marked_le line 404
  30. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.globalComplex_marked_ge line 430
  31. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.globalComplex_marked_eq line 459
  32. lemma OAI.BassTrace.Sparse.Cuts.coe_filter_mem line 479
  33. lemma OAI.BassTrace.Sparse.Cuts.respectsSet_face line 484
  34. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.globalComplex_carrier_in line 499
  35. lemma OAI.BassTrace.Sparse.Cuts.LocalCutData.globalComplex_preserves_respects line 516
  36. structure OAI.BassTrace.Sparse.Cuts.UniversalCuts line 545
  37. def OAI.BassTrace.Sparse.Cuts.UniversalCuts.onComplex line 557
  38. def OAI.BassTrace.Sparse.Cuts.UniversalCuts.localFaces line 560
  39. lemma OAI.BassTrace.Sparse.Cuts.UniversalCuts.mem_global_iff line 564
  40. lemma OAI.BassTrace.Sparse.Cuts.UniversalCuts.restrict_eq_of_restrict_eq line 588