OAI/Topology/ArtinGroups/Harmonic/ResidueEarlierLower.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.sourceResidueAllowed_trans line 13
2. lemma OAI.HarmonicArtin.sourceResidue_strict_height_drop line 31
3. abbrev OAI.HarmonicArtin.SourceResidueEarlierLower line 38
4. def OAI.HarmonicArtin.sourceResidueNegative line 42
5. lemma OAI.HarmonicArtin.sourceResidueNegative_nonempty line 45
6. lemma OAI.HarmonicArtin.sourceResidueNegative_shared line 55
7. def OAI.HarmonicArtin.sourceResidueClose line 62
8. lemma OAI.HarmonicArtin.le_sourceResidueClose line 66
9. lemma OAI.HarmonicArtin.sourceResidueClose_le line 73
10. lemma OAI.HarmonicArtin.sourceResidueClose_strict line 79
11. lemma OAI.HarmonicArtin.sourceResidueClose_monotone line 99
12. lemma OAI.HarmonicArtin.sourceResidueClose_eq line 112
13. def OAI.HarmonicArtin.sourceResidueLowerInclusion line 125
14. def OAI.HarmonicArtin.sourceResidueLowerProjection line 132
15. def OAI.HarmonicArtin.sourceResidueLowerEquiv line 139