OAI/Topology/ArtinGroups/Harmonic/PositiveRegion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.PositiveRegion line 13
2. lemma OAI.HarmonicArtin.positiveRegion_face_closed line 16
3. lemma OAI.HarmonicArtin.positiveRegion_subset_of_factor line 23
4. theorem OAI.HarmonicArtin.spherical_positiveRegions_directed line 34
5. theorem OAI.HarmonicArtin.spherical_positiveRegion_contains_finset line 52