OAI/Topology/ArtinGroups/ParabolicIntersections/RelativeEligibleWithin.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.ParabolicIntersections.RelativeEligibleWithin line 12
2. instance OAI.HarmonicArtin.ParabolicIntersections.relativeEligibleWithinTop line 15
3. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeEligibleProduct_left line 19
4. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeEligibleProduct_right line 41
5. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeEligibleProduct_condition line 63
6. def OAI.HarmonicArtin.ParabolicIntersections.relativeEligibleProductFun line 92
7. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeEligibleProductFun_le_iff line 103
8. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeEligibleProductFun_surjective line 112
9. def OAI.HarmonicArtin.ParabolicIntersections.relativeEligibleProduct line 127
10. def OAI.HarmonicArtin.ParabolicIntersections.relativeEligiblePuncture line 137