OAI/Topology/ArtinGroups/ParabolicIntersections/PointedResidueActive.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCosetVector_upper_antitone_int line 20
2. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCosetVector_upper_monotone_int line 32
3. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueHeight_lt_of_ne line 44
4. def OAI.HarmonicArtin.ParabolicIntersections.pointedResidueActive line 58
5. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueActive_misses line 61
6. abbrev OAI.HarmonicArtin.ParabolicIntersections.PointedResidueEarlierUpper line 74
7. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueUpper_meets line 77
8. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueUpper_active line 93
9. def OAI.HarmonicArtin.ParabolicIntersections.pointedResidueUpperTop line 98
10. def OAI.HarmonicArtin.ParabolicIntersections.pointedResidueUpperClip line 104
11. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueUpperClip_le line 108
12. lemma OAI.HarmonicArtin.ParabolicIntersections.le_pointedResidueUpperClip line 115
13. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueUpperTop_mem line 123
14. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueUpperClip_mem line 150
15. def OAI.HarmonicArtin.ParabolicIntersections.pointedResidueUpperRetraction line 164
16. theorem OAI.HarmonicArtin.ParabolicIntersections.pointedResidueEarlierUpper_contractible line 173