OAI/Topology/ArtinGroups/Complexes/TestUpperBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.TestUpperBound line 15
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.testUpperBound_mono line 19
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.testUpperBound_transport line 23
4. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.positiveTwist_testUpperBound line 29
5. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.positiveTwist_testUpperBound_reflect line 40
6. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.positiveTwist_testUpperBound_iff line 55
7. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.positiveTwist_other_testUpperBound line 76
8. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.generatorBound_of_test_and_outside line 85