OAI/Topology/ArtinGroups/Harmonic/Incidence.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.sourceIncidence line 14
2. lemma OAI.HarmonicArtin.sourceIncidence_incident line 17
3. lemma OAI.HarmonicArtin.source_incidence_le line 24
4. lemma OAI.HarmonicArtin.source_no_incidence line 28
5. def OAI.HarmonicArtin.sourceUpperLevel line 40
6. lemma OAI.HarmonicArtin.sourceIncidence_le_upperLevel line 43
7. lemma OAI.HarmonicArtin.sourceUpperLevel_attained line 47
8. lemma OAI.HarmonicArtin.sourceCosetVector_eq_of_upper_rows line 56
9. lemma OAI.HarmonicArtin.sourceCosetVector_eq_above_upper line 70
10. lemma OAI.HarmonicArtin.sourceCosetSign_eq_above_upper line 76