OAI/Topology/ArtinGroups/Harmonic/Harmonic.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.framed_spherical_posDef line 13
2. def OAI.HarmonicArtin.sourceHarmonicAt line 31
3. lemma OAI.HarmonicArtin.sourceHarmonicAt_outside line 34
4. lemma OAI.HarmonicArtin.sourceHarmonicAt_nonneg line 38
5. lemma OAI.HarmonicArtin.sourceHarmonicAt_harmonic line 43
6. lemma OAI.HarmonicArtin.sourceHarmonicAt_frame line 48
7. lemma OAI.HarmonicArtin.sourceHarmonicAt_invariant line 54
8. lemma OAI.HarmonicArtin.rightCoset_self line 64
9. lemma OAI.HarmonicArtin.sourceHarmonicAt_of_mem line 69
10. def OAI.HarmonicArtin.sourceCosetRepresentative line 75
11. lemma OAI.HarmonicArtin.sourceCosetRepresentative_spec line 79
12. def OAI.HarmonicArtin.sourceCosetVector line 83
13. lemma OAI.HarmonicArtin.sourceCosetVector_eq line 86
14. lemma OAI.HarmonicArtin.sourceCosetVector_nonneg line 91
15. lemma OAI.HarmonicArtin.sourceCosetVector_frame line 95