OAI/Topology/ArtinGroups/Harmonic/CosetBelow.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.sourceCoset_le_iff line 12
2. lemma OAI.HarmonicArtin.sourceCoset_representative_le_iff line 26
3. lemma OAI.HarmonicArtin.sourceSplit_types line 32
4. lemma OAI.HarmonicArtin.sourceSplit_inter line 51
5. lemma OAI.HarmonicArtin.sourceSplit_difference line 70
6. lemma OAI.HarmonicArtin.sourceSplit_coset_le line 81
7. abbrev OAI.HarmonicArtin.SourceCosetBelow line 104
8. def OAI.HarmonicArtin.sourceBelowOffset line 107
9. lemma OAI.HarmonicArtin.sourceBelowOffset_rep line 112
10. def OAI.HarmonicArtin.sourceCosetProductFun line 116
11. lemma OAI.HarmonicArtin.sourceCosetProductFun_le_iff line 132
12. lemma OAI.HarmonicArtin.sourceCosetProductFun_eq_of_reps line 162
13. lemma OAI.HarmonicArtin.sourceCosetProductFun_surjective line 187
14. def OAI.HarmonicArtin.sourceCosetProduct line 223