OAI/Topology/ArtinGroups/Functors/ProbeEmbeddingMap.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.classMap line 18
2. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.classMap_complex line 24
3. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.classMap_positiveTwist line 28
4. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.classMap_negativeTwist line 36
5. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.placement_injective line 46
6. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.generatorArray_core line 52
7. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.levelArray_core line 63
8. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.levelArray_leaf line 73
9. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.classGeneratorArray_core line 83
10. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.classLevelArray_core line 94
11. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.classLevelArray_leaf line 105