OAI/Topology/ArtinGroups/ParabolicIntersections/PointedResidueRank.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueHeight_range_finite line 18
2. def OAI.HarmonicArtin.ParabolicIntersections.pointedResidueRank line 27
3. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueRank_strictMono line 30
4. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueRank_lt_iff line 38
5. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueRank_eq_iff line 53
6. def OAI.HarmonicArtin.ParabolicIntersections.pointedResidueSecondary line 66
7. def OAI.HarmonicArtin.ParabolicIntersections.pointedResidueKey line 69
8. def OAI.HarmonicArtin.ParabolicIntersections.PointedResidueEarlier line 74
9. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueKey_injective line 77
10. theorem OAI.HarmonicArtin.ParabolicIntersections.pointedResidueEarlier_wellFounded line 84
11. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueEarlier_iff line 88
12. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueEarlier_lower_negative line 99
13. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueEarlier_upper_negative line 113
14. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueEarlier_lower_zero line 131
15. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueEarlier_upper_zero line 141