OAI/Topology/ArtinGroups/Realizations/WeightUpperCone.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicArtin.weightUpperCone line 13
  2. lemma OAI.HarmonicArtin.weightUpperCone_support line 18
  3. lemma OAI.HarmonicArtin.weightUpperCone_value line 27
  4. def OAI.HarmonicArtin.Geometric.fullCoxeterFace line 41
  5. lemma OAI.HarmonicArtin.Geometric.fullCoxeterFace_vertices line 45
  6. lemma OAI.HarmonicArtin.Geometric.fullCoxeterFace_polytope line 54
  7. lemma OAI.HarmonicArtin.Geometric.face_le_full line 59
  8. theorem OAI.HarmonicArtin.Geometric.face_barycentric_surjective line 63
  9. lemma OAI.HarmonicArtin.Geometric.barycentric_point_mem line 84
  10. def OAI.HarmonicArtin.Geometric.permutahedronBarycentric line 90
  11. lemma OAI.HarmonicArtin.Geometric.permutahedronBarycentric_continuous line 93
  12. lemma OAI.HarmonicArtin.Geometric.permutahedronBarycentric_bijective line 97
  13. def OAI.HarmonicArtin.Geometric.permutahedronBarycentricHomeomorph line 108
  14. lemma OAI.HarmonicArtin.Geometric.permutahedronBarycentricHomeomorph_apply line 113
  15. lemma OAI.HarmonicArtin.Geometric.barycentric_point_face_iff line 116