OAI/Topology/ArtinGroups/ParabolicIntersections/PointedResidueEarlierLower.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueAllowed_trans line 19
2. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidue_strict_height_drop line 37
3. abbrev OAI.HarmonicArtin.ParabolicIntersections.PointedResidueEarlierLower line 44
4. def OAI.HarmonicArtin.ParabolicIntersections.pointedResidueNegative line 48
5. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueNegative_nonempty line 51
6. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueNegative_shared line 61
7. def OAI.HarmonicArtin.ParabolicIntersections.pointedResidueClose line 68
8. lemma OAI.HarmonicArtin.ParabolicIntersections.le_pointedResidueClose line 72
9. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueClose_le line 79
10. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueClose_strict line 85
11. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueClose_monotone line 105
12. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueClose_eq line 118
13. def OAI.HarmonicArtin.ParabolicIntersections.pointedResidueLowerInclusion line 131
14. def OAI.HarmonicArtin.ParabolicIntersections.pointedResidueLowerProjection line 138
15. def OAI.HarmonicArtin.ParabolicIntersections.pointedResidueLowerEquiv line 145