OAI/Topology/ArtinGroups/Harmonic/PrismFlag.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicArtin.linearMap_insertNth line 12
  2. lemma OAI.HarmonicArtin.collapse_insertNth line 23
  3. lemma OAI.HarmonicArtin.succAbove_le_castSucc_iff line 32
  4. def OAI.HarmonicArtin.prismFlag line 42
  5. lemma OAI.HarmonicArtin.flag_insertNth line 45
  6. lemma OAI.HarmonicArtin.simplex_map_weights line 60
  7. lemma OAI.HarmonicArtin.prismSimplex_collapse line 70
  8. lemma OAI.HarmonicArtin.prismSimplex_time line 83
  9. lemma OAI.HarmonicArtin.simplex_insertNth_decomp line 98
  10. lemma OAI.HarmonicArtin.simplex_flag_nonneg_le_one line 107
  11. def OAI.HarmonicArtin.prismMarginals line 116
  12. lemma OAI.HarmonicArtin.prismMarginals_coordinates line 122
  13. lemma OAI.HarmonicArtin.prismMarginals_prefix line 137
  14. lemma OAI.HarmonicArtin.prismMarginals_cell line 146
  15. lemma OAI.HarmonicArtin.prismSimplex_marginals line 156
  16. lemma OAI.HarmonicArtin.prismMarginals_simplex line 176