OAI/Topology/ArtinGroups/Harmonic/TieCode.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.sourceHeight_eq_blocks line 11
2. lemma OAI.HarmonicArtin.sourceHeight_ne_of_lt line 16
3. lemma OAI.HarmonicArtin.sourceDeligne_countable line 29
4. def OAI.HarmonicArtin.sourceTieCode line 40
5. lemma OAI.HarmonicArtin.sourceTieCode_injective line 45
6. def OAI.HarmonicArtin.sourceVertexKey line 50
7. def OAI.HarmonicArtin.SourceEarlier line 53
8. lemma OAI.HarmonicArtin.sourceVertexKey_injective line 55
9. theorem OAI.HarmonicArtin.sourceEarlier_wellFounded line 60
10. lemma OAI.HarmonicArtin.sourceEarlier_trichotomy line 63
11. lemma OAI.HarmonicArtin.sourceEarlier_iff_of_comparable line 70