OAI/Topology/ArtinGroups/Functors/BasePath.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.basePath line 16
2. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.basePath_source line 21
3. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.basePath_target line 24
4. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.basePath_length line 27
5. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.liftPath line 31
6. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.liftPath_source line 38
7. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.liftPath_target line 43
8. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.basePath_liftPath line 51
9. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.liftPath_length line 56
10. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.path_allowed line 61
11. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.liftPath_basePath line 69
12. abbrev OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.LeftPaths line 77
13. abbrev OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.RightPaths line 80
14. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.leftPathsEquiv line 83
15. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.rightPathsEquiv line 115
16. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.leftPathIndex line 147
17. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.rightPathIndex line 150
18. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.linearMap_liftPath line 156