OAI/RingTheory/BassTrace/ZeroCarriers.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Canonical affine polyhedral cutting and coning in a real vector space, without manifold or cross-simplex metric compatibility assumptions.

  1. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.face_in_zero_carrier line 33
  2. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.flagged_cofaces_card_le_two line 50
  3. def OAI.BassTrace.Sparse.Cuts.PointFiltration.pointedFlags line 66
  4. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.pointedFlags_head line 74
  5. lemma OAI.BassTrace.Sparse.Cuts.PointFiltration.pointedFlags_card line 92