OAI/Topology/ArtinGroups/Geometry/ChamberPoint.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicArtin.simple_mem_coxeterParabolic_iff line 15
  2. lemma OAI.HarmonicArtin.CoxeterCellFace.le_iff_vertices line 29
  3. instance OAI.HarmonicArtin.CoxeterCellFace.(instance at line 45) line 45
  4. instance OAI.HarmonicArtin.CoxeterCellFace.vertices_nonempty line 50
  5. instance OAI.HarmonicArtin.CoxeterCellFace.vertices_fintype line 51
  6. def OAI.HarmonicArtin.Geometric.chamberPoint line 59
  7. lemma OAI.HarmonicArtin.Geometric.chamberPoint_spec line 63
  8. def OAI.HarmonicArtin.Geometric.orbitPoint line 67
  9. lemma OAI.HarmonicArtin.Geometric.orbitPoint_inj line 69
  10. def OAI.HarmonicArtin.Geometric.permutahedron line 72
  11. def OAI.HarmonicArtin.Geometric.faceCoefficient line 74
  12. lemma OAI.HarmonicArtin.Geometric.faceCoefficient_nonneg line 77
  13. lemma OAI.HarmonicArtin.Geometric.faceCoefficient_zero line 81
  14. def OAI.HarmonicArtin.Geometric.faceCovector line 84
  15. def OAI.HarmonicArtin.Geometric.faceLevel line 88
  16. lemma OAI.HarmonicArtin.Geometric.faceCovector_orbit line 91
  17. lemma OAI.HarmonicArtin.Geometric.faceCovector_bound line 96
  18. lemma OAI.HarmonicArtin.Geometric.faceCovector_eq_iff line 102
  19. def OAI.HarmonicArtin.Geometric.facePolytope line 110
  20. lemma OAI.HarmonicArtin.Geometric.facePolytope_eq_level line 113
  21. lemma OAI.HarmonicArtin.Geometric.orbit_mem_facePolytope line 125
  22. lemma OAI.HarmonicArtin.Geometric.facePolytope_mono line 131
  23. lemma OAI.HarmonicArtin.Geometric.facePolytope_subset_iff line 134
  24. def OAI.HarmonicArtin.Geometric.faceCenter line 140
  25. lemma OAI.HarmonicArtin.Geometric.faceCenter_mem line 143
  26. lemma OAI.HarmonicArtin.Geometric.faceCenter_covector_le line 149
  27. lemma OAI.HarmonicArtin.Geometric.faceCenter_covector_eq_iff line 153
  28. theorem OAI.HarmonicArtin.Geometric.orbit_support_face line 160