OAI/Topology/ArtinGroups/Harmonic/PrismPrefix.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicArtin.prismPrefix line 11
  2. def OAI.HarmonicArtin.PrismCell line 14
  3. lemma OAI.HarmonicArtin.continuous_prismPrefix line 17
  4. lemma OAI.HarmonicArtin.prismCell_closed line 21
  5. lemma OAI.HarmonicArtin.prismPrefix_nonneg line 27
  6. lemma OAI.HarmonicArtin.prismPrefix_add line 30
  7. lemma OAI.HarmonicArtin.prismPrefix_last line 35
  8. lemma OAI.HarmonicArtin.prismPrefix_zero line 42
  9. lemma OAI.HarmonicArtin.prismPrefix_succ line 48
  10. lemma OAI.HarmonicArtin.prismCell_cover line 58
  11. def OAI.HarmonicArtin.prismLeft line 87
  12. lemma OAI.HarmonicArtin.prismLeft_nonneg line 90
  13. lemma OAI.HarmonicArtin.prismLeft_le line 92
  14. lemma OAI.HarmonicArtin.prismLeft_cell line 94
  15. def OAI.HarmonicArtin.prismWeights line 98
  16. def OAI.HarmonicArtin.prismSimplex line 102