OAI/Topology/ArtinGroups/ParabolicIntersections/PointedResidueEarlierLowerIso.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueEarlier_total line 27
2. def OAI.HarmonicArtin.ParabolicIntersections.pointedResidueEarlierLowerIso line 32
3. def OAI.HarmonicArtin.ParabolicIntersections.pointedResidueEarlierUpperIso line 45
4. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidue_lower_boundary line 57
5. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidue_upper_weights_contractible line 71
6. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidue_emptyLink_upper line 81
7. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidue_emptyLink_lower line 89