OAI/Topology/ArtinGroups/Geometry/OrbitHalfspace.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.Geometric.permutahedron_compact line 14
2. def OAI.HarmonicArtin.Geometric.orbitHalfspace line 17
3. lemma OAI.HarmonicArtin.Geometric.chamberCovector_basis line 20
4. lemma OAI.HarmonicArtin.Geometric.orbitHalfspace_bound line 23
5. lemma OAI.HarmonicArtin.Geometric.permutahedron_halfspaces line 32
6. lemma OAI.HarmonicArtin.Geometric.support_face_of_attains line 58
7. theorem OAI.HarmonicArtin.Geometric.face_boundary_step line 78