OAI/Topology/ArtinGroups/Harmonic/PeakSupport.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.sourcePeakSupport line 12
2. def OAI.HarmonicArtin.sourcePeak line 15
3. lemma OAI.HarmonicArtin.sourcePeakSupport_mem line 18
4. lemma OAI.HarmonicArtin.sourcePeak_bound line 26
5. lemma OAI.HarmonicArtin.sourcePeak_above line 30
6. lemma OAI.HarmonicArtin.sourcePeak_nonzero line 35
7. lemma OAI.HarmonicArtin.sourcePeak_positive line 44
8. lemma OAI.HarmonicArtin.sourcePeak_nonzero_of_pos line 51
9. def OAI.HarmonicArtin.sourceLowerLevel line 59
10. lemma OAI.HarmonicArtin.sourcePeak_le_lowerLevel line 62
11. lemma OAI.HarmonicArtin.sourceLowerLevel_attained line 68
12. lemma OAI.HarmonicArtin.sourceCosetVector_eq_of_lower_open line 90
13. lemma OAI.HarmonicArtin.sourceCosetVector_lower_comparison line 108
14. lemma OAI.HarmonicArtin.sourceCosetVector_lower_comparison_rev line 122
15. lemma OAI.HarmonicArtin.sourceCosetVector_eq_above_lower line 136
16. lemma OAI.HarmonicArtin.sourceBlock_eq_above_lower line 143