OAI/Topology/ArtinGroups/Geometry/StrictLinearBoundInterior.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.Geometric.strict_linear_bound_of_interior line 12
2. lemma OAI.HarmonicArtin.Geometric.proper_face_covector_ne_zero line 35
3. lemma OAI.HarmonicArtin.Geometric.proper_face_subset_frontier line 43
4. lemma OAI.HarmonicArtin.Geometric.frontier_active_halfspace line 55
5. lemma OAI.HarmonicArtin.Geometric.orbitHalfspace_strict_vertex line 73
6. theorem OAI.HarmonicArtin.Geometric.permutahedron_frontier_faces line 82