OAI/Topology/ArtinGroups/Harmonic/IsolatedIterationData.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.HarmonicArtin.IsolatedIterationData line 31
2. abbrev OAI.HarmonicArtin.IsolatedIterationData.region line 56
3. abbrev OAI.HarmonicArtin.IsolatedIterationData.operated line 57
4. def OAI.HarmonicArtin.IsolatedIterationData.capped line 58
5. def OAI.HarmonicArtin.IsolatedIterationData.openSocle line 60
6. lemma OAI.HarmonicArtin.IsolatedIterationData.boundary line 63
7. abbrev OAI.HarmonicArtin.IsolatedIterationData.fullRegion line 67
8. lemma OAI.HarmonicArtin.IsolatedIterationData.capJ line 70
9. lemma OAI.HarmonicArtin.IsolatedIterationData.separation line 78
10. lemma OAI.HarmonicArtin.IsolatedIterationData.lower_bound_move line 89
11. lemma OAI.HarmonicArtin.IsolatedIterationData.socle_below line 96
12. lemma OAI.HarmonicArtin.IsolatedIterationData.cap_move line 101