OAI/Topology/ArtinGroups/Harmonic/PuncturedBoundaryIso.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.puncturedBoundaryIso line 13
2. def OAI.HarmonicArtin.positiveCellEmbedding line 29
3. lemma OAI.HarmonicArtin.positiveCellEmbedding_full line 36
4. def OAI.HarmonicArtin.positivePuncturedBoundaryIso line 44
5. lemma OAI.HarmonicArtin.restriction_sphericalLongest line 51
6. lemma OAI.HarmonicArtin.restrictedArtinHom_positiveLift line 67